X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitamakeLib.ml;h=f811c84e2ecd56d633a6430d01ae933f62024b6e;hb=cf45f0f766c147324e587522a4a3761b5ac13415;hp=47dbdb22ba6e679a536150609c63610e8b1f4071;hpb=bc9899a797f5d6e8e37a76923172d18c774e7573;p=helm.git diff --git a/helm/software/matita/matitamakeLib.ml b/helm/software/matita/matitamakeLib.ml index 47dbdb22b..f811c84e2 100644 --- a/helm/software/matita/matitamakeLib.ml +++ b/helm/software/matita/matitamakeLib.ml @@ -75,7 +75,12 @@ let initialize () = match root with | None -> () | Some root -> - developments := {root = root ; name = name} :: !developments) + developments := {root = root ; name = name} :: !developments; + let inc = Helm_registry.get_list + Helm_registry.string "matita.includes" in + Helm_registry.set_list Helm_registry.of_string + ~key:"matita.includes" ~value:(inc @ [root]) + ) l (* finds the makefile path for development devel *) @@ -96,12 +101,11 @@ let development_for_dir dir = false else let pref = String.sub d2 0 len1 in - pref = d1 + pref = d1 && (len1 = len2 || d2.[len1] = '/') in - (* it must be unique *) try Some (List.find (fun d -> is_prefix_of d.root dir) !developments) - with Not_found -> None + with Not_found | Failure _ -> None let development_for_name name = try @@ -202,7 +206,7 @@ let call_make ?matita_flags development target make = let args = ["--no-print-directory"; "-s"; "-k"; "-f"; makefile; target] @ flags in -(* prerr_endline (String.concat " " args); *) + (* prerr_endline (String.concat " " args); *) make development.root args let build_development ?matita_flags ?(target="all") development =