]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/matita/matitamakeLib.ml
Removed debugging print.
[helm.git] / helm / matita / matitamakeLib.ml
index 8dc45faaaff1d75877d93d83ac699b3e42303a4f..48d6696281248cda435447c4f59a55e38936668c 100644 (file)
@@ -125,12 +125,10 @@ let rebuild_makefile development =
   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
   
@@ -269,7 +267,6 @@ let destroy_development development =
     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