# HG changeset patch
# User wenzelm
# Date 1611177626 -3600
# Node ID 68f0bd0c8e875c5bcde330e51e5a1e1fc2b9acce
# Parent  be9b73dfd3e0e8f05e8344b441306ff280c382fc
more informative error;
tuned;

diff -r be9b73dfd3e0 -r 68f0bd0c8e87 src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Wed Jan 20 09:46:01 2021 +0100
+++ b/src/Pure/Admin/build_history.scala	Wed Jan 20 22:20:26 2021 +0100
@@ -575,7 +575,7 @@
       else {
         val afp_repos = isabelle_repos_other + Path.explode("AFP")
         Mercurial.setup_repository(afp_repos_source, afp_repos, ssh = ssh)
-          " -A " + Bash.string(afp_rev.get)
+        " -A " + Bash.string(afp_rev.get)
       }
 
 
@@ -585,11 +585,19 @@
     {
       val output_file = tmp_dir + Path.explode("output")
 
-      execute("Admin/build_history",
-        "-o " + ssh.bash_path(output_file) +
-          (if (rev == "") "" else " -r " + Bash.string(rev_id)) + " " +
-          options + afp_options + " " + ssh.bash_path(isabelle_repos_other) + " " + args,
-        echo = true, strict = false)
+      val rev_options = if (rev == "") "" else " -r " + Bash.string(rev_id)
+
+      try {
+        execute("Admin/build_history",
+          "-o " + ssh.bash_path(output_file) + rev_options + afp_options + " " + options + " " +
+            ssh.bash_path(isabelle_repos_other) + " " + args,
+          echo = true, strict = false)
+      }
+      catch {
+        case ERROR(msg) =>
+          cat_error(msg,
+            "The error(s) above occurred for build_bistory " + rev_options + afp_options)
+      }
 
       for (line <- split_lines(ssh.read(output_file)))
       yield {