diff --git a/Jenkinsfile b/Jenkinsfile index 958b46590f..7f72724f25 100644 --- a/Jenkinsfile +++ b/Jenkinsfile @@ -4,6 +4,12 @@ pipeline { } stages { + stage('Check formatting') { + steps { + echo 'Checking formatting...' + sh 'bash -c "tools/check_format.sh 2>&1 >(tee tools/check_format.txt)"' + } + } stage('Setup') { steps { sh 'cp /usr/local/etc/roms/baserom_oot.z64 baseroms/gc-eu-mq-dbg/baserom.z64' @@ -56,6 +62,9 @@ pipeline { } } post { + failure { + sh 'cat tools/check_format.txt' + } always { echo "Finished, deleting directory." deleteDir() diff --git a/tools/check_format.sh b/tools/check_format.sh new file mode 100755 index 0000000000..1195a9c593 --- /dev/null +++ b/tools/check_format.sh @@ -0,0 +1,23 @@ +#!/bin/bash + +STATUSOLD=`git status --porcelain` +./format.py -j +if [ $? -ne 0 ] +then + echo "Formatter failed. Exiting." + exit -1 +fi +STATUSNEW=`git status --porcelain` + +if [ "${STATUSOLD}" != "${STATUSNEW}" ]; +then + echo "" + echo "Misformatted files found. Run ./format.py and verify codegen is not impacted." + echo "" + diff --unified=0 --label "Old git status" <(echo "${STATUSOLD}") --label "New git status" <(echo "${STATUSNEW}") + echo "" + echo "Exiting." + exit 1 +fi + +exit 0