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")) +