diff -r 12abaffb0346 -r 932b2a7139e2 src/Pure/General/path.scala --- a/src/Pure/General/path.scala Sun Nov 12 12:26:08 2023 +0100 +++ b/src/Pure/General/path.scala Sun Nov 12 12:33:22 2023 +0100 @@ -327,8 +327,8 @@ def is_file: Boolean = file.isFile def is_dir: Boolean = file.isDirectory - def check_file: Path = if (is_file) this else error("No such file: " + this) - def check_dir: Path = if (is_dir) this else error("No such directory: " + this) + def check_file: Path = if (is_file) this else error("No such file: " + this.expand) + def check_dir: Path = if (is_dir) this else error("No such directory: " + this.expand) def java_path: JPath = file.toPath