equal
deleted
inserted
replaced
10 - val ml_system = "alice"; |
10 - val ml_system = "alice"; |
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 |
|
16 use "ML-Systems/no_multithreading.ML"; |
|
17 |
15 |
18 |
16 fun exit 0 = (OS.Process.exit OS.Process.success): unit |
19 fun exit 0 = (OS.Process.exit OS.Process.success): unit |
17 | exit _ = OS.Process.exit OS.Process.failure; |
20 | exit _ = OS.Process.exit OS.Process.failure; |
18 |
21 |
19 |
22 |