src/Pure/Tools/build.ML
changeset 65306 eab556c6037d
parent 65058 3e9f382fb67e
child 65307 c1ba192b4f96
--- a/src/Pure/Tools/build.ML	Sat Mar 18 14:16:13 2017 +0100
+++ b/src/Pure/Tools/build.ML	Sat Mar 18 14:30:03 2017 +0100
@@ -201,6 +201,6 @@
           (Par_Exn.release_all [res1, res2]; "") handle exn =>
             (Runtime.exn_message exn handle _ (*sic!*) =>
               "Exception raised, but failed to print details!");
-    in Output.protocol_message (Markup.build_theories_result id) [result] end);
+    in Output.protocol_message (Markup.build_theories_result id) [result] end | _ => raise Match);
 
 end;