equal
deleted
inserted
replaced
871 else if hd (explode file) = "/" then file |
871 else if hd (explode file) = "/" then file |
872 else "/" ^ space_implode "/" |
872 else "/" ^ space_implode "/" |
873 (rm_points (space_explode "/" (tack_on cwd file)) []) |
873 (rm_points (space_explode "/" (tack_on cwd file)) []) |
874 end; |
874 end; |
875 |
875 |
|
876 fun file_exists file = (file_info file <> ""); |
|
877 |
876 |
878 |
877 (** misc functions **) |
879 (** misc functions **) |
878 |
880 |
879 (*use the keyfun to make a list of (x, key) pairs*) |
881 (*use the keyfun to make a list of (x, key) pairs*) |
880 fun make_keylist (keyfun: 'a->'b) : 'a list -> ('a * 'b) list = |
882 fun make_keylist (keyfun: 'a->'b) : 'a list -> ('a * 'b) list = |