# HG changeset patch
# User wenzelm
# Date 1495789885 -7200
# Node ID 83c44969f431f69914c1dc3038d892aef9639230
# Parent  9a28fc03c3fefaf022550f057a33a1642e953a9b
do not expose ML interrupt in Scala;

diff -r 9a28fc03c3fe -r 83c44969f431 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 =