From a7644dab8bada9dc5d7a4112a8934bd40380ec18 Mon Sep 17 00:00:00 2001
From: Waldemar Zurowski <waldemar.zurowski@r3.com>
Date: Fri, 19 Jun 2020 22:09:02 +0100
Subject: [PATCH] Cosmetic change for Windows Server builds

---
 .ci/dev/mswin/Jenkinsfile | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/.ci/dev/mswin/Jenkinsfile b/.ci/dev/mswin/Jenkinsfile
index f09522578b..ffbfbcb5d6 100644
--- a/.ci/dev/mswin/Jenkinsfile
+++ b/.ci/dev/mswin/Jenkinsfile
@@ -28,8 +28,12 @@ pipeline {
         ansiColor('xterm')
         timestamps()
         timeout(time: 3, unit: 'HOURS')
-//        overrideIndexTriggers true // works as expected for PRs
-//        overrideIndexTriggers false // works as expected for non PRs
+
+        /*
+         * a bit awkward to read
+         * is parameter is true  -> push events are *not* ignored
+         * if parameter is false -> push events *are* ignored
+         */
         overrideIndexTriggers (!isReleaseBranch)
     }