# HG changeset patch
# User lcp
# Date 793902470 -3600
# Node ID 61fcac0e50fc6210e9abe294ecbca346a1ba45fa
# Parent  6cd9c397f36ad5e395b0d57046d9278abfdeb86d
exit: new, for use in Makefiles

diff -r 6cd9c397f36a -r 61fcac0e50fc src/Pure/NJ.ML
--- a/src/Pure/NJ.ML	Mon Feb 27 17:11:25 1995 +0100
+++ b/src/Pure/NJ.ML	Mon Feb 27 17:27:50 1995 +0100
@@ -8,8 +8,9 @@
 
 (*** Poly/ML emulation ***)
 
-(*To exit the system -- an alternative to ^D *)
-fun quit () = System.Unsafe.CInterface.exit 0;
+(*To exit the system with an exit code -- an alternative to ^D *)
+val exit = System.Unsafe.CInterface.exit;
+fun quit () = exit 0;
 
 (*To change the current directory*)
 val cd = System.Directory.cd;