Merge remote-tracking branch 'origin/ci-jenkinsfile-modifs' into integration_2023_w18b

This commit is contained in:
Robert Schmidt
2023-05-08 11:52:47 +02:00
9 changed files with 0 additions and 9 deletions
-1
View File
@@ -36,7 +36,6 @@ pipeline {
label nodeExecutor
}
options {
disableConcurrentBuilds()
timestamps()
gitLabConnection('OAI GitLab')
ansiColor('xterm')