# HG changeset patch
# User wenzelm
# Date 1478009565 -3600
# Node ID 075c077a6e2900b95855f83f40bbed93bcacf8a5
# Parent  b52141002646bc6c125a66cbef5460ebd6716b5c
ignore interrupts from underlying process, e.g. due to out-of-memory situation in ML_Process (see also build.scala);

diff -r b52141002646 -r 075c077a6e29 src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Tue Nov 01 15:00:27 2016 +0100
+++ b/src/Pure/Admin/build_history.scala	Tue Nov 01 15:12:45 2016 +0100
@@ -433,7 +433,8 @@
         ssh.bash_path(isabelle_admin + Path.explode("build_history")) + " " + options + " " +
           ssh.bash_path(isabelle_repos_other) + " " + args,
         progress_stdout = progress_stdout _,
-        progress_stderr = progress.echo(_))
+        progress_stderr = progress.echo(_),
+        strict = false)
 
     (result.toList, process_result)
   }