--- a/src/Pure/Tools/update_comments.scala Sun Jan 14 20:39:27 2018 +0100
+++ b/src/Pure/Tools/update_comments.scala Sun Jan 14 20:58:41 2018 +0100
@@ -20,8 +20,8 @@
case tok :: rest if tok.source == "--" || tok.source == Symbol.comment =>
rest.dropWhile(_.is_space) match {
case tok1 :: rest1 if tok1.is_text =>
- val res = Symbol.comment + Symbol.space + Library.cartouche(tok1.content)
- update(rest1, res :: result)
+ val txt = Symbol.trim_blanks(tok1.content)
+ update(rest1, (Symbol.comment + Symbol.space + Library.cartouche(txt)) :: result)
case _ => update(rest, tok.source :: result)
}
case tok :: rest => update(rest, tok.source :: result)