ignore interrupts from underlying process, e.g. due to out-of-memory situation in ML_Process (see also build.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)
   }