src/Pure/Admin/build_history.scala
changeset 77368 7c57d9586f4c
parent 77207 d98a99e4eea9
child 77783 fb61887c069a
--- a/src/Pure/Admin/build_history.scala	Fri Feb 24 20:23:48 2023 +0100
+++ b/src/Pure/Admin/build_history.scala	Fri Feb 24 20:40:50 2023 +0100
@@ -582,7 +582,7 @@
     else {
       ssh.with_tmp_dir { tmp_dir =>
         val output_file = tmp_dir + Path.explode("output")
-        val build_options = (if (afp_repos.isEmpty) "" else " -A") + " " + options
+        val build_options = if_proper(afp_repos, " -A") + " " + options
         try {
           val script =
             ssh.bash_path(Path.explode("Admin/build_other")) +