From 193e93e30ad38fed80b8891cd323375aa85b6c2e Mon Sep 17 00:00:00 2001
From: Gabriele C <sgdc3.mail@gmail.com>
Date: Tue, 13 Mar 2018 12:46:23 +0100
Subject: [PATCH] Whoops, damn escape character

---
 Jenkinsfile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Jenkinsfile b/Jenkinsfile
index 57ff8cc9..f2c117d7 100644
--- a/Jenkinsfile
+++ b/Jenkinsfile
@@ -8,7 +8,7 @@ pipeline {
         stage ('prepare') {
             steps {
                 env.CI_SKIP = "false"
-                result = sh (script: "git log -1 | grep '(?s).[CI[-\s]SKIP].*'", returnStatus: true)
+                result = sh (script: "git log -1 | grep '(?s).[CI[-\\s]SKIP].*'", returnStatus: true)
                 if (result == 0) {
                     env.CI_SKIP = "true"
                     error "'[CI-SKIP]' found in git commit message. Aborting."