# HG changeset patch
# User wenzelm
# Date 1567777505 -7200
# Node ID 44588e355ca8adde80d1deaef6efd791a1a963fd
# Parent  4655897b828724a9f3296b31d48bc2d7237457dd
more robust;

diff -r 4655897b8287 -r 44588e355ca8 src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Fri Sep 06 11:32:38 2019 +0200
+++ b/src/Pure/Tools/dump.scala	Fri Sep 06 15:45:05 2019 +0200
@@ -131,7 +131,7 @@
     val deps: Sessions.Deps =
       Sessions.load_structure(dump_options, dirs = dirs, select_dirs = select_dirs).
         selection_deps(dump_options, selection, progress = progress,
-          uniform_session = true, loading_sessions = true)
+          uniform_session = true, loading_sessions = true).check_errors
 
     val resources: Headless.Resources =
       Headless.Resources.make(dump_options, logic, progress = progress, log = log,