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) {