From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 20 Apr 2007 13:30:16 +0000 (+0000)
Subject: developments root are now part of default inclusion paths;
X-Git-Tag: 0.4.95@7852~510
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e85f44f9159792f670ca831e239a17d9ed3a9a70;p=helm.git

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 b7b4151fa..eb33e49b8 100644
--- 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 471f26970..553e1176f 100644
--- 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 *)