more robust on Windows, where C:\\ and \\SERVER\SHARE cause problems (line 920 of winbasicio.cpp);
authorwenzelm
Fri, 03 Feb 2023 14:10:09 +0100
changeset 77180 7af930cd0fce
parent 77179 6d2ca97a8f46
child 77181 3eb3de867786
more robust on Windows, where C:\\ and \\SERVER\SHARE cause problems (line 920 of winbasicio.cpp);
src/Pure/General/file.ML
--- 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;