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 **)