--- a/src/Pure/System/getopts.scala Sat Jul 17 22:50:25 2021 +0200
+++ b/src/Pure/System/getopts.scala Sat Jul 17 23:09:54 2021 +0200
@@ -18,8 +18,8 @@
option_specs.foldLeft(Map.empty[Char, (Boolean, String => Unit)]) {
case (m, (s, f)) =>
val (a, entry) =
- if (s.size == 1) (s(0), (false, f))
- else if (s.size == 2 && s.endsWith(":")) (s(0), (true, f))
+ if (s.length == 1) (s(0), (false, f))
+ else if (s.length == 2 && s.endsWith(":")) (s(0), (true, f))
else error("Bad option specification: " + quote(s))
if (m.isDefinedAt(a)) error("Duplicate option specification: " + quote(a.toString))
else m + (a -> entry)