| changeset 65827 | 3bba3856b56c |
| parent 61276 | 8a4bd05c1735 |
| child 67880 | e59220a075de |
--- a/src/Pure/Tools/check_keywords.scala Sun May 14 17:00:57 2017 +0200 +++ b/src/Pure/Tools/check_keywords.scala Sun May 14 17:01:05 2017 +0200 @@ -46,9 +46,8 @@ }, parallel_args).flatten for ((tok, pos) <- bad) { - progress.echo(Output.warning_text( - "keyword conflict: " + tok.kind.toString + " " + quote(tok.content) + - Position.here(pos))) + progress.echo_warning( + "keyword conflict: " + tok.kind.toString + " " + quote(tok.content) + Position.here(pos)) } } }