author | wenzelm |
Sat, 23 May 2020 11:25:34 +0200 | |
changeset 71867 | 3ee14fc25736 |
parent 71866 | 081fdd53003a |
child 71868 | 06ec50d9fc0a |
--- 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 */