From e85f44f9159792f670ca831e239a17d9ed3a9a70 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 20 Apr 2007 13:30:16 +0000 Subject: [PATCH] developments root are now part of default inclusion paths; incluson path used to include something is printed (to understand what is gouing on) --- components/grafite_parser/dependenciesParser.ml | 4 +++- matita/matitamakeLib.ml | 7 ++++++- 2 files changed, 9 insertions(+), 2 deletions(-) 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 *) -- 2.39.2