diff --git a/Jenkinsfile b/Jenkinsfile index cf5d8f3b63..50cd889087 100644 --- a/Jenkinsfile +++ b/Jenkinsfile @@ -3,6 +3,10 @@ pipeline { label 'mm' } + options { + ansiColor('xterm') + } + stages { stage('Check formatting') { steps {