changeset 66873 | 9953ae603a23 |
parent 66712 | 4c98c929a12a |
child 67219 | 81e9804b2014 |
--- a/src/Pure/Tools/build.ML Mon Oct 16 14:21:14 2017 +0200 +++ b/src/Pure/Tools/build.ML Mon Oct 16 14:32:09 2017 +0200 @@ -92,6 +92,8 @@ | NONE => ()) else () end + else if function = Markup.theory_timing then + inline_message (#2 function) args else (case Markup.dest_loading_theory props of SOME name => writeln ("\floading_theory = " ^ name)