From: Daniel Arndt Date: Fri, 9 Jul 2021 14:52:13 +0000 (-0400) Subject: Delete indent step in CI X-Git-Tag: v9.4.0-rc1~1119^2~1 X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=d11f4f8a65e6a4551374df77c9662b3123710ba6;p=dealii.git Delete indent step in CI --- diff --git a/Jenkinsfile b/Jenkinsfile index 232bad2dda..d89e19e47c 100644 --- a/Jenkinsfile +++ b/Jenkinsfile @@ -60,34 +60,6 @@ pipeline githubNotify context: 'CI', description: 'running tests...', status: 'PENDING' } } - - stage("indent") - { - post { - failure { - githubNotify context: 'indent', description: 'failed', status: 'FAILURE' - } - } - - steps - { - // we are finally running, so we can mark the 'ready' context from Jenkinsfile.mark as success: - githubNotify context: 'ready', description: ':-)', status: 'SUCCESS' - - // We can not use 'indent' because we are missing the master branch: - // "fatal: ambiguous argument 'master': unknown revision or path" - sh ''' - ./contrib/utilities/indent-all - ''' - sh 'git diff > changes.diff' - archiveArtifacts artifacts: 'changes.diff', fingerprint: true - sh ''' - git diff --exit-code || \ - { echo "Please check indentation, see artifacts at the top right!"; exit 1; } - ''' - githubNotify context: 'indent', description: '', status: 'SUCCESS' - } - } } }