| changeset 41944 | b97091ae583a |
| parent 40785 | c755df0f7062 |
| child 42003 | 6e45dc518ebb |
--- a/src/Pure/General/file.ML Sun Mar 13 15:16:37 2011 +0100 +++ b/src/Pure/General/file.ML Sun Mar 13 16:01:00 2011 +0100 @@ -68,7 +68,7 @@ fun check path = if exists path then () - else error ("No such file or directory: " ^ quote (Path.implode path)); + else error ("No such file or directory: " ^ Path.print path); val rm = OS.FileSys.remove o platform_path;