| changeset 77180 | 7af930cd0fce | 
| parent 76884 | a004c5322ea4 | 
--- 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;