# HG changeset patch
# User lcp
# Date 795261399 -3600
# Node ID aa0c5f9daf5babdfec80d9328581cf4d6968ff81
# Parent  d3f734f661417d66f2d59cf4b6d383348ed2ca20
Declares the function exit_use to behave like use but fail if
errors are detected.  It can be used in all Makefiles except Pure, which will
write the exception handler explicitly ("exit" will have been declared
already).

diff -r d3f734f66141 -r aa0c5f9daf5b src/Pure/library.ML
--- a/src/Pure/library.ML	Wed Mar 15 10:53:58 1995 +0100
+++ b/src/Pure/library.ML	Wed Mar 15 10:56:39 1995 +0100
@@ -692,6 +692,8 @@
   (writeln ("\n**** Starting " ^ fname ^ " ****"); use fname;
    writeln ("\n**** Finished " ^ fname ^ " ****")));
 
+(*For Makefiles: use the file, but exit with error code if errors found.*)
+fun exit_use fname = use fname handle _ => exit 1;
 
 
 (** filenames **)