src/HOL/Mirabelle/lib/Tools/mirabelle
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