--- a/src/Pure/Tools/build.ML Fri Apr 01 16:32:20 2016 +0200
+++ b/src/Pure/Tools/build.ML Fri Apr 01 17:00:18 2016 +0200
@@ -81,8 +81,11 @@
val name = the_default "" (Properties.get args Markup.nameN);
val pos = Position.of_properties args;
val {elapsed, ...} = Markup.parse_timing_properties args;
+ val is_significant =
+ Timing.is_relevant_time elapsed andalso
+ Time.>= (elapsed, Options.default_seconds "command_timing_threshold");
in
- if Timing.is_relevant_time elapsed then
+ if is_significant then
(case approximative_id name pos of
SOME id => inline_message (#2 function) (Markup.command_timing_properties id elapsed)
| NONE => ())