changeset 71867 | 3ee14fc25736 |
parent 71866 | 081fdd53003a |
child 73344 | f5c147654661 |
--- a/src/Pure/General/word.scala Sat May 23 10:58:01 2020 +0200 +++ b/src/Pure/General/word.scala Sat May 23 11:25:34 2020 +0200 @@ -77,7 +77,7 @@ explode(_ == sep, text) def explode(text: String): List[String] = - explode(Character.isWhitespace(_), text) + explode(Character.isWhitespace _, text) /* brackets */