developments root are now part of default inclusion paths;

incluson path used to include something is printed (to understand what is gouing on)

diff --git a/components/grafite_parser/dependenciesParser.ml b/components/grafite_parser/dependenciesParser.ml
index b7b4151fa3b5c47f874cd476f60012e9bcfe7f85..eb33e49b80d7b5f453dbadb433851f7de3e96556 100644 (file)
--- a/components/grafite_parser/dependenciesParser.ml
+++ b/components/grafite_parser/dependenciesParser.ml
@@ -83,7 +83,9 @@ let make_absolute paths path =
    | p :: tl ->
       let path = p ^ "/" ^ path in
        try
-         ignore (Unix.stat path); path
+         ignore (Unix.stat path);
+         HLog.debug ("Including "^path^" with path: " ^ p);
+         path
        with Unix.Unix_error _ -> aux tl
    in
    try

diff --git a/matita/matitamakeLib.ml b/matita/matitamakeLib.ml
index 471f26970f403f6470d6c61c59c5d7519b0e44c1..553e1176fe21df83355923d3ca1f8b8506333c2a 100644 (file)
--- a/matita/matitamakeLib.ml
+++ b/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 *)