# HG changeset patch
# User lcp
# Date 793903664 -3600
# Node ID 822e5749161206a38f3a0ec3fee51a96a92cbfaa
# Parent  5de21942d0466e6940f093243beb4c575aedfc2e
Added the exception handler
handle _ => exit 1.  This will catch all errors and force an exit with error
code, causing Make to fail.

diff -r 5de21942d046 -r 822e57491612 src/ZF/IMP/ROOT.ML
--- a/src/ZF/IMP/ROOT.ML	Mon Feb 27 17:44:43 1995 +0100
+++ b/src/ZF/IMP/ROOT.ML	Mon Feb 27 17:47:44 1995 +0100
@@ -17,4 +17,4 @@
 writeln"Root file for ZF/IMP";
 proof_timing := true;
 loadpath := [".","IMP"];
-time_use_thy "Equiv";
+time_use_thy "Equiv" handle _ => exit 1;