From 3a2ae576a3e5a56caed936bebbef62a381929b94 Mon Sep 17 00:00:00 2001 From: Daniel Arndt Date: Thu, 8 Dec 2022 10:56:43 -0500 Subject: [PATCH] Fix indentation in Jenkinsfile.mpi --- contrib/ci/Jenkinsfile.mpi | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/contrib/ci/Jenkinsfile.mpi b/contrib/ci/Jenkinsfile.mpi index e54df7d7b1..948bd233c8 100644 --- a/contrib/ci/Jenkinsfile.mpi +++ b/contrib/ci/Jenkinsfile.mpi @@ -57,12 +57,12 @@ pipeline { when { not { - anyOf { - branch 'master' - branch pattern: "dealii-*", comparator: "GLOB" - } + anyOf { + branch 'master' + branch pattern: "dealii-*", comparator: "GLOB" + } } - } + } steps { @@ -124,7 +124,7 @@ pipeline sh "cp /home/dealii/build/detailed.log $WORKSPACE/detailed-mpi.log || true" archiveArtifacts artifacts: 'detailed-mpi.log', fingerprint: true } - + failure { githubNotify context: 'Jenkins: MPI', description: 'build failed', status: 'FAILURE' -- 2.39.5