Declares the function exit_use to behave like use but fail if
authorlcp
Wed Mar 15 10:56:39 1995 +0100 (1995-03-15)
changeset 955aa0c5f9daf5b
parent 954 d3f734f66141
child 956 cc929b9ddc80
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).
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Wed Mar 15 10:53:58 1995 +0100
     1.2 +++ b/src/Pure/library.ML	Wed Mar 15 10:56:39 1995 +0100
     1.3 @@ -692,6 +692,8 @@
     1.4    (writeln ("\n**** Starting " ^ fname ^ " ****"); use fname;
     1.5     writeln ("\n**** Finished " ^ fname ^ " ****")));
     1.6  
     1.7 +(*For Makefiles: use the file, but exit with error code if errors found.*)
     1.8 +fun exit_use fname = use fname handle _ => exit 1;
     1.9  
    1.10  
    1.11  (** filenames **)