# HG changeset patch
# User wenzelm
# Date 1675429809 -3600
# Node ID 7af930cd0fce203fc8541b7d051b13fc19aea07b
# Parent  6d2ca97a8f466e835aab327381101c31f3a8cd32
more robust on Windows, where C:\\ and \\SERVER\SHARE cause problems (line 920 of winbasicio.cpp);

diff -r 6d2ca97a8f46 -r 7af930cd0fce 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;