more robust: defer error in sessions structure to build process;
authorwenzelm
Mon, 25 Jan 2021 22:30:39 +0100
changeset 73184 a5998396051e
parent 73183 ebf7babc05ce
child 73185 b310b93563f6
more robust: defer error in sessions structure to build process;
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)
       }