more robust: avoid -D ~~/AFP/thys after crash of AFP.init (notably in AFP/1001c0dfced0);
authorwenzelm
Sat, 17 Jul 2021 22:50:25 +0200
changeset 74036 57768f30d17c
parent 74035 ec3249dd63dd
child 74037 c13198575f75
more robust: avoid -D ~~/AFP/thys after crash of AFP.init (notably in AFP/1001c0dfced0);
src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Sat Jul 17 22:17:27 2021 +0200
+++ b/src/Pure/Admin/build_history.scala	Sat Jul 17 22:50:25 2021 +0200
@@ -164,11 +164,15 @@
     val (afp_build_args, afp_sessions) =
       if (afp_rev.isEmpty) (Nil, Nil)
       else {
-        val (opt, sessions) =
-          try {
-            val afp = AFP.init(options, afp_repos)
-            ("-d", afp.partition(afp_partition))
-          } catch { case ERROR(_) => ("-D", Nil) }
+        val (opt, sessions) = {
+          if (afp_partition == 0) ("-d", Nil)
+          else {
+            try {
+              val afp = AFP.init(options, afp_repos)
+              ("-d", afp.partition(afp_partition))
+            } catch { case ERROR(_) => ("-D", Nil) }
+          }
+        }
         (List(opt, "~~/AFP/thys"), sessions)
       }