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