changeset 60745 | d86b4cd0f1ec |
parent 60744 | 4eba53a0ac3d |
child 60852 | 1c51a2ca8204 |
--- a/src/Pure/ML-Systems/ml_debugger_polyml-5.5.3.ML Fri Jul 17 16:23:25 2015 +0200 +++ b/src/Pure/ML-Systems/ml_debugger_polyml-5.5.3.ML Fri Jul 17 16:43:53 2015 +0200 @@ -29,6 +29,3 @@ val debug_name_space = PolyML.DebuggerInterface.debugNameSpace; end; - -fun ml_debugger_parameters false = [] - | ml_debugger_parameters true = [PolyML.Compiler.CPDebug true];