| changeset 60954 | eeee8349e9eb |
| parent 60953 | 87f0f707a5f8 |
| child 60956 | 10d463883dc2 |
--- a/src/Pure/ML-Systems/polyml.ML Sun Aug 16 23:14:27 2015 +0200 +++ b/src/Pure/ML-Systems/polyml.ML Mon Aug 17 15:19:25 2015 +0200 @@ -206,5 +206,6 @@ (* ML debugger *) -use "ML-Systems/ml_debugger.ML"; -if ML_System.name = "polyml-5.5.3" then use "ML-Systems/ml_debugger_polyml-5.5.3.ML" else (); +if ML_System.name = "polyml-5.5.3" +then use "ML-Systems/ml_debugger_polyml-5.5.3.ML" +else use "ML-Systems/ml_debugger.ML";