changeset 60954 | eeee8349e9eb |
parent 60953 | 87f0f707a5f8 |
child 60956 | 10d463883dc2 |
60953:87f0f707a5f8 | 60954:eeee8349e9eb |
---|---|
204 struct_name ^ ".ML_print_depth ())))))"; |
204 struct_name ^ ".ML_print_depth ())))))"; |
205 |
205 |
206 |
206 |
207 (* ML debugger *) |
207 (* ML debugger *) |
208 |
208 |
209 use "ML-Systems/ml_debugger.ML"; |
209 if ML_System.name = "polyml-5.5.3" |
210 if ML_System.name = "polyml-5.5.3" then use "ML-Systems/ml_debugger_polyml-5.5.3.ML" else (); |
210 then use "ML-Systems/ml_debugger_polyml-5.5.3.ML" |
211 else use "ML-Systems/ml_debugger.ML"; |