author | wenzelm |
Mon, 24 Oct 2016 11:48:32 +0200 | |
changeset 64368 | 364d74ea985f |
parent 64367 | a424f2737646 |
child 64369 | 6a9816764b37 |
--- a/src/Pure/Admin/check_sources.scala Mon Oct 24 11:42:39 2016 +0200 +++ b/src/Pure/Admin/check_sources.scala Mon Oct 24 11:48:32 2016 +0200 @@ -41,7 +41,7 @@ Output.warning("CR character" + Position.here(file_pos)) if (Word.bidi_detect(content)) - Output.warning("Bidirectional Unicode text " + Position.here(file_pos)) + Output.warning("Bidirectional Unicode text" + Position.here(file_pos)) } def check_hg(root: Path)