do not expose ML interrupt in Scala;
authorwenzelm
Fri, 26 May 2017 11:11:25 +0200
changeset 65931 83c44969f431
parent 65930 9a28fc03c3fe
child 65932 db5e701b691a
do not expose ML interrupt in Scala;
src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Fri May 26 11:09:16 2017 +0200
+++ b/src/Pure/Admin/build_history.scala	Fri May 26 11:11:25 2017 +0200
@@ -207,7 +207,7 @@
       val build_args1 = List("-v", "-j" + processes) ::: build_args
       val build_result =
         (new Other_Isabelle(build_out_progress, hg.root, isabelle_identifier))(
-          "build " + Bash.strings(build_args1), redirect = true, echo = true)
+          "build " + Bash.strings(build_args1), redirect = true, echo = true, strict = false)
       val build_end = Date.now()
 
       val build_info: Build_Log.Build_Info =