equal
deleted
inserted
replaced
80 fun copy_dir src dst = scala_function "copy_dir" [src, dst]; |
80 fun copy_dir src dst = scala_function "copy_dir" [src, dst]; |
81 |
81 |
82 fun copy_file src dst = scala_function "copy_file" [src, dst]; |
82 fun copy_file src dst = scala_function "copy_file" [src, dst]; |
83 |
83 |
84 fun copy_file_base (base_dir, src) target_dir = |
84 fun copy_file_base (base_dir, src) target_dir = |
85 scala_function "copy_file_base" [base_dir, src, target_dir]; |
85 scala_function0 "copy_file_base" |
|
86 [absolute_path base_dir, Path.implode src, absolute_path target_dir]; |
86 |
87 |
87 |
88 |
88 (* tmp files *) |
89 (* tmp files *) |
89 |
90 |
90 fun create_tmp_path name ext = |
91 fun create_tmp_path name ext = |