| changeset 78243 | 0e221a8128e4 |
| parent 75394 | 42267c650205 |
| child 79510 | d8330439823a |
--- a/src/Pure/General/scan.scala Sun Jul 02 18:56:52 2023 +0200 +++ b/src/Pure/General/scan.scala Sun Jul 02 19:05:59 2023 +0200 @@ -73,10 +73,10 @@ repeated(pred, 0, 1) def many(pred: Symbol.Symbol => Boolean): Parser[String] = - repeated(pred, 0, Integer.MAX_VALUE) + repeated(pred, 0, Int.MaxValue) def many1(pred: Symbol.Symbol => Boolean): Parser[String] = - repeated(pred, 1, Integer.MAX_VALUE) + repeated(pred, 1, Int.MaxValue) /* character */