| changeset 26656 | 62fff5feb756 | 
| parent 26503 | 4dec4460244f | 
| child 26946 | 0b6eff8c088d | 
--- a/src/Pure/General/file.ML Tue Apr 15 16:12:13 2008 +0200 +++ b/src/Pure/General/file.ML Tue Apr 15 16:12:15 2008 +0200 @@ -141,7 +141,7 @@ fun eq paths = (case try (pairself (OS.FileSys.fileId o platform_path)) paths of - SOME ids => OS.FileSys.compare ids = EQUAL + SOME ids => is_equal (OS.FileSys.compare ids) | NONE => false); fun copy src dst =