changeset 76548 | 0af64cc2eee9 |
parent 76547 | 9fe5d8c70352 |
child 76550 | a82fc7755ba5 |
--- a/src/Pure/System/components.scala Wed Nov 30 21:53:55 2022 +0100 +++ b/src/Pure/System/components.scala Wed Nov 30 22:07:59 2022 +0100 @@ -131,6 +131,9 @@ split_lines(File.read(components)).filter(_.nonEmpty) def write_components(lines: List[String]): Unit = File.write(components, terminate_lines(lines)) + + def write_settings(text: String): Unit = + File.write(settings, "# -*- shell-script -*- :mode=shellscript:\n" + text) }