src/Pure/System/options.scala
changeset 78908 f38153e58f21
parent 78614 4da5cdaa4dcd
child 78909 65acbafc70e5
--- a/src/Pure/System/options.scala	Sun Nov 05 19:55:18 2023 +0100
+++ b/src/Pure/System/options.scala	Tue Nov 07 12:02:34 2023 +0100
@@ -29,6 +29,9 @@
       }
 
     def print(name: String, value: String): String = Properties.Eq(name, print_value(value))
+
+    def bash_strings(opts: Iterable[Spec]): String =
+      opts.iterator.map(opt => "-o " + Bash.string(opt.toString)).mkString(" ", " ", " ")
   }
 
   sealed case class Spec(name: String, value: Option[String] = None, permissive: Boolean = false) {