changeset 59083 | 88b0b1f28adc |
parent 58872 | f0f623005324 |
child 61463 | 8e46cea6a45a |
--- a/src/Pure/Tools/update_header.scala Wed Dec 03 11:50:58 2014 +0100 +++ b/src/Pure/Tools/update_header.scala Wed Dec 03 14:04:38 2014 +0100 @@ -13,7 +13,7 @@ { val text0 = File.read(path) val text1 = - (for (tok <- Outer_Syntax.empty.scan(text0).iterator) + (for (tok <- Token.explode(Keyword.Keywords.empty, text0).iterator) yield { if (tok.source == "header") section else tok.source }).mkString if (text0 != text1) {