Check for sessions with quick_and_dirty mode enabled.
ci/woodpecker/push/build Pipeline was successful Details

This commit is contained in:
Achim D. Brucker 2023-03-02 08:43:57 +00:00
parent de4c7a5168
commit baf1d1b629
2 changed files with 31 additions and 0 deletions

View File

@ -4,6 +4,7 @@ pipeline:
commands:
- ./.woodpecker/check_dangling_theories
- ./.woodpecker/check_external_file_refs
- ./.woodpecker/check_quick_and_dirty -w
- export ARTIFACT_DIR=$CI_WORKSPACE/.artifacts/$CI_REPO/$CI_BRANCH/$CI_BUILD_NUMBER/$LATEX
- mkdir -p $ARTIFACT_DIR
- export `isabelle getenv ISABELLE_HOME_USER`

View File

@ -0,0 +1,30 @@
#!/bin/bash
set -e
failuremsg="Error"
failurecode=1
while [ $# -gt 0 ]
do
case "$1" in
--warning|-w)
failuremsg="Warning"
failurecode=0;;
esac
shift
done
echo "Checking for sessions with quick_and_dirty mode enabled:"
echo "========================================================"
rootlist=`find -name 'ROOT' -exec grep -l 'quick_and_dirty *= *true' {} \;`
if [ -z "$rootlist" ] ; then
echo " * Success: No sessions with quick_and_dirty mode enabled found."
exit 0
else
echo -e "$rootlist"
echo "$failuremsg: Sessions with quick_and_dirty mode enabled found (see list above)!"
exit $failurecode
fi