more robust: avoid -D ~~/AFP/thys after crash of AFP.init (notably in AFP/1001c0dfced0);
--- 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)
}