| changeset 73340 | 0ffcad1f6130 |
| parent 72763 | 3cc73d00553c |
| child 74887 | 56247fdb8bbb |
--- a/src/Pure/Tools/update_comments.scala Mon Mar 01 20:12:09 2021 +0100 +++ b/src/Pure/Tools/update_comments.scala Mon Mar 01 22:22:12 2021 +0100 @@ -12,7 +12,7 @@ object Update_Comments { - def update_comments(path: Path) + def update_comments(path: Path): Unit = { def make_comment(tok: Token): String = Symbol.comment + Symbol.space + Symbol.cartouche(Symbol.trim_blanks(tok.content))