diff -r 186e07be32c3 -r a004c5322ea4 src/Pure/Admin/check_sources.scala --- a/src/Pure/Admin/check_sources.scala Tue Jan 03 15:42:25 2023 +0100 +++ b/src/Pure/Admin/check_sources.scala Tue Jan 03 16:05:07 2023 +0100 @@ -10,7 +10,7 @@ object Check_Sources { def check_file(path: Path): Unit = { val file_name = path.implode - val file_pos = Position.File(path.implode_symbolic) + val file_pos = Position.File(File.symbolic_path(path)) def line_pos(i: Int) = Position.Line_File(i + 1, file_name) if (space_explode('/', Word.lowercase(path.expand.drop_ext.implode)).contains("aux"))