# HG changeset patch
# User wenzelm
# Date 883320429 -3600
# Node ID 8648ba842d14db71c00c23a36f3fdc17c00a7235
# Parent  7e5611945959ca47b38f298febaef5e12bea151e
improved error handling;

diff -r 7e5611945959 -r 8648ba842d14 src/Pure/mk
--- a/src/Pure/mk	Sun Dec 28 15:46:13 1997 +0100
+++ b/src/Pure/mk	Sun Dec 28 15:47:09 1997 +0100
@@ -85,7 +85,7 @@
 
   $ISABELLE \
     -e "val ml_system = \"$ML_SYSTEM\";" \
-    -e "use\"$COMPAT\"; use\"ROOT.ML\" handle _ => exit 1;" \
+    -e "(use\"$COMPAT\"; use\"ROOT.ML\") handle _ => exit 1;" \
     -q -w RAW_ML_SYSTEM Pure > $LOG 2>&1
 else
   ITEM="RAW"
@@ -94,7 +94,7 @@
 
   $ISABELLE \
     -e "val ml_system = \"$ML_SYSTEM\";" \
-    -e "use\"$COMPAT\";" \
+    -e "use\"$COMPAT\" handle _ => exit 1;;" \
     -q -w RAW_ML_SYSTEM RAW > $LOG 2>&1
 fi