# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1717520155 -7200
# Node ID 6ae378791c5298fe7072d330ec52a4294b0f5f00
# Parent  8ae6f4e8cc2ab76f27ee7eff48a192f26ef29027
read prefs properly;

diff -r 8ae6f4e8cc2a -r 6ae378791c52 src/Pure/Build/build_manager.scala
--- a/src/Pure/Build/build_manager.scala	Tue Jun 04 18:43:04 2024 +0200
+++ b/src/Pure/Build/build_manager.scala	Tue Jun 04 18:55:55 2024 +0200
@@ -344,7 +344,7 @@
                 case _ => None
               }
 
-            stmt.string(7) = get(user_build => Options.Spec.bash_strings(user_build.prefs))
+            stmt.string(7) = get(user_build => user_build.prefs.map(_.print).mkString(","))
             stmt.bool(8) = get(_.requirements)
             stmt.bool(9) = get(_.all_sessions)
             stmt.string(10) = get(_.base_sessions.mkString(","))