changeset 73359 | d8a0e996614b |
parent 71601 | 97ccf48c2f0c |
child 74037 | c13198575f75 |
--- a/src/Pure/System/getopts.scala Wed Mar 03 22:48:46 2021 +0100 +++ b/src/Pure/System/getopts.scala Thu Mar 04 15:41:46 2021 +0100 @@ -15,7 +15,7 @@ def apply(usage_text: String, option_specs: (String, String => Unit)*): Getopts = { val options = - (Map.empty[Char, (Boolean, String => Unit)] /: option_specs) { + option_specs.foldLeft(Map.empty[Char, (Boolean, String => Unit)]) { case (m, (s, f)) => val (a, entry) = if (s.size == 1) (s(0), (false, f))