changeset 42034 | a77df5241959 |
parent 40976 | 8df0a190df1e |
child 42069 | 6a147393c62a |
--- a/src/HOL/Mirabelle/lib/Tools/mirabelle Mon Mar 21 12:43:23 2011 +0100 +++ b/src/HOL/Mirabelle/lib/Tools/mirabelle Mon Mar 21 12:43:25 2011 +0100 @@ -56,6 +56,12 @@ exit 1 } +function fail() +{ + echo "$1" >&2 + exit 2 +} + ## process command line @@ -103,6 +109,6 @@ for FILE in "$@" do - perl -w "$MIRABELLE_HOME/lib/scripts/mirabelle.pl" "$FILE" + perl -w "$MIRABELLE_HOME/lib/scripts/mirabelle.pl" "$FILE" || fail "Mirabelle failed." done