# HG changeset patch
# User wenzelm
# Date 1666467512 -7200
# Node ID 640ab184efb465269c3530dba36399989cf34b16
# Parent  24e951a8a3187e72aaaf04e201c5bd1fcb32984a
tuned;

diff -r 24e951a8a318 -r 640ab184efb4 src/Pure/Admin/build_history.scala
--- 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),