fix build

2023-06-27 16:27:18 +02:00
parent fd71d1f38e
commit d7efeb8d59
1 changed files with 8 additions and 0 deletions
--- a/Jenkinsfile.develop
+++ b/Jenkinsfile.develop
@@ -9,4 +9,12 @@ pipeline {
      }
    }
  }
+  post {
+    success {
+      postSuccess();
+    }
+    always {
+      postAlways();
+    }
+  }
 }