# HG changeset patch
# User wenzelm
# Date 1592050654 -7200
# Node ID 12f455cc657325b01748f77e9b597baa4907e39f
# Parent  82b00b8f18716283d2d4927672e0e9e25193d7f7
clarified errors;

diff -r 82b00b8f1871 -r 12f455cc6573 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)