author | paulson |
Fri, 09 Jul 2004 11:13:36 +0200 | |
changeset 15028 | f6a22afe0134 |
parent 15027 | d23887300b96 |
child 15029 | a4d0ed993050 |
--- 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;