Post the style patch

espressomd · Apr 21, 2020 · 6efa9da · 6efa9da
1 parent cf6b380
commit 6efa9da
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/maintainer/CI/fix_style.sh b/maintainer/CI/fix_style.sh
@@ -25,7 +25,7 @@ if ! git diff-index --quiet HEAD -- && [ "${1}" != "-f" ]; then
     exit 1
 fi
 
-maintainer/lint/pre_commit.sh run --all-files || exit 1
+maintainer/lint/pre_commit.sh run --all-files
 
 if [ "${CI}" != "" ]; then
     git --no-pager diff > style.patch