| changeset 19473 | d87a8838afa4 |
| parent 18715 | f809deffdd8f |
| child 19960 | a0e3f2df9b0e |
--- a/src/Pure/General/file.ML Wed Apr 26 20:34:11 2006 +0200 +++ b/src/Pure/General/file.ML Wed Apr 26 22:38:05 2006 +0200 @@ -103,7 +103,7 @@ fun mkdir path = system_command ("mkdir -p " ^ shell_path path); fun is_dir path = - if_none (try OS.FileSys.isDir (platform_path path)) false; + the_default false (try OS.FileSys.isDir (platform_path path)); (* read / write files *)