# HG changeset patch
# User wenzelm
# Date 1546108008 -3600
# Node ID a1e8bcda8cecb2238268d1e4484628037d5d7b0d
# Parent  da2726f78610c3b58fad0951239cb32ea5f37c58
tuned signature;

diff -r da2726f78610 -r a1e8bcda8cec src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sat Dec 29 18:45:57 2018 +0100
+++ b/src/Pure/Tools/build.scala	Sat Dec 29 19:26:48 2018 +0100
@@ -844,14 +844,18 @@
     progress: Progress = No_Progress,
     build_heap: Boolean = false,
     dirs: List[Path] = Nil,
-    system_mode: Boolean = false): Int =
+    system_mode: Boolean = false,
+    strict: Boolean = false): Int =
   {
-    if (build(options, build_heap = build_heap, no_build = true, dirs = dirs,
-        system_mode = system_mode, sessions = List(logic)).ok) 0
-    else {
-      progress.echo("Build started for Isabelle/" + logic + " ...")
-      Build.build(options, progress = progress, build_heap = build_heap, dirs = dirs,
-        system_mode = system_mode, sessions = List(logic)).rc
-    }
+    val rc =
+      if (build(options, build_heap = build_heap, no_build = true, dirs = dirs,
+          system_mode = system_mode, sessions = List(logic)).ok) 0
+      else {
+        progress.echo("Build started for Isabelle/" + logic + " ...")
+        Build.build(options, progress = progress, build_heap = build_heap, dirs = dirs,
+          system_mode = system_mode, sessions = List(logic)).rc
+      }
+
+    if (strict && rc != 0) error("Failed to build Isabelle/" + logic) else rc
   }
 }
diff -r da2726f78610 -r a1e8bcda8cec src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Sat Dec 29 18:45:57 2018 +0100
+++ b/src/Pure/Tools/dump.scala	Sat Dec 29 19:26:48 2018 +0100
@@ -212,8 +212,8 @@
     system_mode: Boolean = false,
     selection: Sessions.Selection = Sessions.Selection.empty)
   {
-    if (Build.build_logic(options, logic, build_heap = true, progress = progress,
-      dirs = dirs ::: select_dirs, system_mode = system_mode) != 0) error(logic + " FAILED")
+    Build.build_logic(options, logic, build_heap = true, progress = progress,
+      dirs = dirs ::: select_dirs, system_mode = system_mode, strict = true)
 
     val dump_options = make_options(options, aspects)