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: make_still_working~6369
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c34321f75d5a01eb8a267916d0ece6670603dd46;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/helm/software/components/grafite_parser/dependenciesParser.ml b/helm/software/components/grafite_parser/dependenciesParser.ml
index b7b4151fa..eb33e49b8 100644
--- a/helm/software/components/grafite_parser/dependenciesParser.ml
+++ b/helm/software/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/helm/software/matita/matitamakeLib.ml b/helm/software/matita/matitamakeLib.ml
index 471f26970..553e1176f 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 *)