equal
deleted
inserted
replaced
267 fun copy_files path1 path2 = |
267 fun copy_files path1 path2 = |
268 (File.mkdir path2; |
268 (File.mkdir path2; |
269 system ("cp " ^ File.sysify_path path1 ^ " " ^ File.sysify_path path2)); (*FIXME: quote!?*) |
269 system ("cp " ^ File.sysify_path path1 ^ " " ^ File.sysify_path path2)); (*FIXME: quote!?*) |
270 |
270 |
271 fun copy_all path1 path2 = |
271 fun copy_all path1 path2 = |
272 (File.mkdir path2; |
272 (File.mkdir path2; |
273 system ("cp -r " ^ File.quote_sysify_path path1 ^ " " ^ |
273 system ("cp -r " ^ File.quote_sysify_path path1 ^ "/. " ^ |
274 File.quote_sysify_path (Path.append path2 Path.parent))); |
274 File.quote_sysify_path path2)); |
275 |
275 |
276 |
276 |
277 fun name_of_session elems = space_implode "/" ("Isabelle" :: elems); |
277 fun name_of_session elems = space_implode "/" ("Isabelle" :: elems); |
278 |
278 |
279 fun init build info doc doc_graph path name doc_prefix2 (remote_path, first_time) verbose = |
279 fun init build info doc doc_graph path name doc_prefix2 (remote_path, first_time) verbose = |