From a58a6ca6a448a37e6f97e133aaa59c6c05e0d5da Mon Sep 17 00:00:00 2001
From: Manuele Simi <manuele.simi@isti.cnr.it>
Date: Wed, 3 Feb 2021 21:37:41 -0500
Subject: [PATCH] Fix param name.

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

diff --git a/Jenkinsfile b/Jenkinsfile
index 88dfd91..cfa3f76 100644
--- a/Jenkinsfile
+++ b/Jenkinsfile
@@ -180,7 +180,7 @@ def exec(repo_url, repo_name) {
              output = sh(script: bashWrapper, returnStdout: true)?.trim()
         }
     }
-    if ((!filter) || (filter_with && output.contains(filter_with))) {
+    if ((!filter_with) || (filter_with && output.contains(filter_with))) {
         def xml_action = """
         <action repo="${repo_url}">
             <stdout>