From f4c4364f00afe2a754204dec387cd80124b15c3a Mon Sep 17 00:00:00 2001
From: krzys-h <krzys_h@interia.pl>
Date: Mon, 29 May 2017 21:08:51 +0200
Subject: [PATCH] Jenkinsfile: prevent PRs to master

I just merged a PR to master by mistake. Whoops! Let's not let that happen again.
---
 Jenkinsfile | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/Jenkinsfile b/Jenkinsfile
index 84e65471..688c3e2b 100644
--- a/Jenkinsfile
+++ b/Jenkinsfile
@@ -5,6 +5,10 @@ if (env.BRANCH_NAME.startsWith('PR-')) {
     properties([[$class: 'BuildDiscarderProperty', strategy: [$class: 'LogRotator', artifactDaysToKeepStr: '30', artifactNumToKeepStr: '5']]])
 }
 
+if (env.CHANGE_TARGET == 'master') {
+    error("This pull request targets the wrong branch. Please reopen the pull request targetting the dev branch.")
+}
+
 node('master') {
     stage('Pull changes') {
         checkout scm