equal
deleted
inserted
replaced
124 fun copy from to = |
124 fun copy from to = |
125 let val target = if is_dir to then Path.append to (Path.base from) else to |
125 let val target = if is_dir to then Path.append to (Path.base from) else to |
126 in write target (read from) end; |
126 in write target (read from) end; |
127 |
127 |
128 fun copy_dir from to = |
128 fun copy_dir from to = |
129 system_command ("cp -r " ^ shell_path from ^ "/. " ^ shell_path to); |
129 (system ("cp -r " ^ shell_path from ^ "/. " ^ shell_path to); ()); (* FIXME system_command *) |
130 |
130 |
131 |
131 |
132 (* use ML files *) |
132 (* use ML files *) |
133 |
133 |
134 val use = use o platform_path; |
134 val use = use o platform_path; |