clarified errors;
authorwenzelm
Sat, 13 Jun 2020 14:17:34 +0200
changeset 71936 12f455cc6573
parent 71935 82b00b8f1871
child 71937 92de7d74b8f8
clarified errors;
src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala	Thu Jun 11 16:13:53 2020 +0100
+++ b/src/Pure/Admin/build_release.scala	Sat Jun 13 14:17:34 2020 +0200
@@ -288,7 +288,7 @@
       val version = proper_string(rev) orElse proper_release_name getOrElse "tip"
       val ident =
         try { hg.id(version) }
-        catch { case ERROR(_) => error("Bad repository version: " + version) }
+        catch { case ERROR(msg) => cat_error("Bad repository version: " + version, msg) }
 
       val dist_version =
         proper_release_name match {
@@ -366,13 +366,13 @@
         other_isabelle.bash(export_classpath + "./Admin/build all", echo = true).check
         other_isabelle.bash(export_classpath + "./bin/isabelle jedit -b", echo = true).check
       }
-      catch { case ERROR(_) => error("Failed to build tools") }
+      catch { case ERROR(msg) => cat_error("Failed to build tools:", msg) }
 
       try {
         other_isabelle.bash(
           "./bin/isabelle build_doc -a -o system_heaps -j " + parallel_jobs, echo = true).check
       }
-      catch { case ERROR(_) => error("Failed to build documentation") }
+      catch { case ERROR(msg) => cat_error("Failed to build documentation:", msg) }
 
       make_news(other_isabelle, release.dist_version)