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;