# HG changeset patch
# User wenzelm
# Date 1626555025 -7200
# Node ID 57768f30d17c4361199ad02a8ab1d88886fc64dd
# Parent  ec3249dd63dd908ea321c439d7e20c8abdf386f5
more robust: avoid -D ~~/AFP/thys after crash of AFP.init (notably in AFP/1001c0dfced0);

diff -r ec3249dd63dd -r 57768f30d17c 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)
       }