src/Pure/Tools/build.ML
changeset 50845 477ca927676f
parent 50777 20126dd9772c
child 50975 73ec6ad6700e
     1.1 --- a/src/Pure/Tools/build.ML	Sat Jan 12 14:56:57 2013 +0100
     1.2 +++ b/src/Pure/Tools/build.ML	Sat Jan 12 15:00:48 2013 +0100
     1.3 @@ -22,7 +22,10 @@
     1.4  fun protocol_message props output =
     1.5    (case ML_statistics props output of
     1.6      SOME stats => writeln ("\fML_statistics = " ^ ML_Syntax.print_properties stats)
     1.7 -  | NONE => raise Fail "Undefined Output.protocol_message");
     1.8 +  | NONE =>
     1.9 +      (case Markup.dest_loading_theory props of
    1.10 +        SOME name => writeln ("\floading_theory = " ^ name)
    1.11 +      | NONE => raise Fail "Undefined Output.protocol_message"));
    1.12  
    1.13  
    1.14  (* build *)