diff --git a/jenkins/scripts/propose_updated_config_file.sh b/jenkins/scripts/propose_updated_config_file.sh index ab53e48903..1bd6f6c989 100755 --- a/jenkins/scripts/propose_updated_config_file.sh +++ b/jenkins/scripts/propose_updated_config_file.sh @@ -64,7 +64,7 @@ if ! git diff --stat --exit-code HEAD ; then git commit $git_args <