equal
deleted
inserted
replaced
11 - use "ML-Systems/alice.ML"; |
11 - use "ML-Systems/alice.ML"; |
12 - use "ROOT.ML"; |
12 - use "ROOT.ML"; |
13 - Session.finish (); |
13 - Session.finish (); |
14 *) |
14 *) |
15 |
15 |
16 use "ML-Systems/no_multithreading.ML"; |
16 use "ML-Systems/exn.ML"; |
|
17 use "ML-Systems/multithreading_dummy.ML"; |
17 |
18 |
18 |
19 |
19 fun exit 0 = (OS.Process.exit OS.Process.success): unit |
20 fun exit 0 = (OS.Process.exit OS.Process.success): unit |
20 | exit _ = OS.Process.exit OS.Process.failure; |
21 | exit _ = OS.Process.exit OS.Process.failure; |
21 |
22 |