let rm = BuildTimeConf.runtime_base_dir ^ "/matitaclean" ^ am_i_opt () in
let mm = BuildTimeConf.runtime_base_dir ^ "/matitadep" ^ am_i_opt () in
let df = pool () ^ development.name ^ "/depend" in
- let dfs = pool () ^ development.name ^ "/depend.short" in
let template = Pcre.replace ~pat:"@ROOT@" ~templ:development.root template in
let template = Pcre.replace ~pat:"@CC@" ~templ:cc template in
let template = Pcre.replace ~pat:"@DEP@" ~templ:mm template in
let template = Pcre.replace ~pat:"@DEPFILE@" ~templ:df template in
- let template = Pcre.replace ~pat:"@DEPFILESHORT@" ~templ:dfs template in
let template = Pcre.replace ~pat:"@CLEAN@" ~templ:rm template in
MatitaMisc.output_file template makefilepath
(* creates a new development if possible *)
let initialize_development name dir =
+ let name = Pcre.replace ~pat:" " ~templ:"_" name in
let dev = {name = name ; root = dir} in
match development_for_dir dir with
| Some d ->
let old = Unix.getcwd () in
try
Unix.chdir chdir;
- let rc = Unix.system (String.concat " " ("make"::args)) in
+ let rc =
+ Unix.system
+ (String.concat " " ("make"::(List.map Filename.quote args)))
+ in
Unix.chdir old;
match rc with
| Unix.WEXITED 0 -> true
let clean_development_in_bg refresh_cb development =
call_make development "clean" (mk_maker refresh_cb)
-let destroy_development development =
+let destroy_development_aux development clean_development =
let delete_development development =
let unlink file =
try
unlink (makefile_for_development development);
unlink (pool () ^ development.name ^ rootfile);
unlink (pool () ^ development.name ^ "/depend");
- unlink (pool () ^ development.name ^ "/depend.short");
rmdir (pool () ^ development.name);
developments :=
List.filter (fun d -> d.name <> development.name) !developments
logger `Warning "This may cause garbage."
end;
delete_development development
+
+let destroy_development development =
+ destroy_development_aux development clean_development
+
+let destroy_development_in_bg refresh development =
+ destroy_development_aux development (clean_development_in_bg refresh)
let root_for_development development = development.root
let name_for_development development = development.name