author | wenzelm |
Fri, 03 Feb 2023 14:10:09 +0100 | |
changeset 77180 | 7af930cd0fce |
parent 77179 | 6d2ca97a8f46 |
child 77181 | 3eb3de867786 |
--- a/src/Pure/General/file.ML Thu Feb 02 12:55:07 2023 +0000 +++ b/src/Pure/General/file.ML Fri Feb 03 14:10:09 2023 +0100 @@ -89,7 +89,7 @@ (* directory entries *) -val exists = can OS.FileSys.modTime o platform_path; +val exists = can OS.FileSys.fileId o platform_path; val rm = OS.FileSys.remove o platform_path;