# HG changeset patch
# User wenzelm
# Date 1611610239 -3600
# Node ID a5998396051ef0564a7272853bb0b1846347bd53
# Parent  ebf7babc05ce2649babc787d65dcdca0cab3f1de
more robust: defer error in sessions structure to build process;

diff -r ebf7babc05ce -r a5998396051e src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Sun Jan 24 19:34:37 2021 +0100
+++ b/src/Pure/Admin/build_history.scala	Mon Jan 25 22:30:39 2021 +0100
@@ -161,8 +161,12 @@
     val (afp_build_args, afp_sessions) =
       if (afp_rev.isEmpty) (Nil, Nil)
       else {
-        val afp = AFP.init(options, afp_repos)
-        (List("-d", "~~/AFP/thys"), afp.partition(afp_partition))
+        val (opt, sessions) =
+          try {
+            val afp = AFP.init(options, afp_repos)
+            ("-d", afp.partition(afp_partition))
+          } catch { case ERROR(_) => ("-D", Nil) }
+        (List(opt, "~~/AFP/thys"), sessions)
       }