author | paulson |
Tue, 22 Jul 1997 11:15:14 +0200 | |
changeset 3539 | d4443afc8d28 |
parent 3538 | ed9de44032e0 |
child 3540 | acd60238f191 |
--- a/src/Pure/ML-Systems/MLWorks.ML Tue Jul 22 11:14:18 1997 +0200 +++ b/src/Pure/ML-Systems/MLWorks.ML Tue Jul 22 11:15:14 1997 +0200 @@ -25,6 +25,8 @@ **) +structure Option = General; + (*To exit the system with an exit code -- an alternative to ^D *) fun exit 0 = OS.Process.exit OS.Process.success | exit _ = OS.Process.exit OS.Process.failure;