Add node name

2025-12-20 18:35:38 +01:00
parent df6d68c8a0
commit 1474ae1885
1 changed files with 1 additions and 1 deletions
--- a/Jenkinsfile.ci
+++ b/Jenkinsfile.ci
@@ -83,7 +83,7 @@ pipeline {

  post {
    always {
-        node {
+        node('principal') {
            cleanWs()
        }
    }