author | Fabian Huch <huch@in.tum.de> |
Tue, 04 Jun 2024 18:55:55 +0200 | |
changeset 80251 | 6ae378791c52 |
parent 80250 | 8ae6f4e8cc2a |
child 80252 | 96543177ab7e |
--- 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(","))