src/Pure/System/components.scala
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)
   }