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) }