equal
deleted
inserted
replaced
70 |
70 |
71 fun copy_file src0 dst0 = |
71 fun copy_file src0 dst0 = |
72 let |
72 let |
73 val src = Path.expand src0; |
73 val src = Path.expand src0; |
74 val dst = Path.expand dst0; |
74 val dst = Path.expand dst0; |
75 val (target_dir, target) = |
75 val target = if File.is_dir dst then Path.append dst (Path.base src) else dst; |
76 if File.is_dir dst then (dst, Path.append dst (Path.base src)) |
|
77 else (Path.dir dst, dst); |
|
78 in |
76 in |
79 if File.eq (src, target) then () |
77 if File.eq (src, target) then () |
80 else |
78 else |
81 (ignore o system_command) |
79 ignore (system_command ("cp -p -f " ^ File.shell_path src ^ " " ^ File.shell_path target)) |
82 ("cp -p -f " ^ File.shell_path src ^ " " ^ File.shell_path target_dir ^ "/.") |
|
83 end; |
80 end; |
84 |
81 |
85 fun copy_file_base (base_dir, src0) target_dir = |
82 fun copy_file_base (base_dir, src0) target_dir = |
86 let |
83 let |
87 val src = Path.expand src0; |
84 val src = Path.expand src0; |