Add file that release builds can use to eliminate timing, if desired
1 files changed, 14 insertions(+), 0 deletions(-) A => timing-release.sml
A => timing-release.sml +14 -0
@@ 0,0 1,14 @@ + +(* Release builds that don't want to include timing measurements may + wish to have this included after timing.sml, in order to eliminate + the timing calls without having to change the rest of the code. *) + +structure Timing : TIMING = struct + + type tag = string + + fun record tag t = () + fun timed tag f = f () + fun summarise level = () + +end