--- a/src/Pure/Admin/build_history.scala Sat Oct 22 21:20:55 2022 +0200
+++ b/src/Pure/Admin/build_history.scala Sat Oct 22 21:38:32 2022 +0200
@@ -506,9 +506,8 @@
more_preferences = more_preferences, verbose = verbose, build_tags = build_tags,
build_args = build_args)
- if (output_file == "") {
- for ((_, log_path) <- results)
- Output.writeln(log_path.implode, stdout = true)
+ if (output_file.isEmpty) {
+ for ((_, log_path) <- results) Output.writeln(log_path.implode, stdout = true)
}
else {
File.write(Path.explode(output_file),