changeset 15028 | f6a22afe0134 |
parent 14870 | c5cf7c001313 |
child 15699 | 7d91dd712ff8 |
--- a/src/Pure/ML-Systems/polyml.ML Thu Jul 08 19:34:56 2004 +0200 +++ b/src/Pure/ML-Systems/polyml.ML Fri Jul 09 11:13:36 2004 +0200 @@ -155,3 +155,13 @@ (case OS.Process.getEnv var of NONE => "" | SOME txt => txt); + + +(* profiling: version that works even with +ML{*profiling 1*} +apply \\<dots> +ML{*profiling 0*} +*) + +val profiling: int->unit = + RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler;