]> matita.cs.unibo.it Git - helm.git/commitdiff
ficed include and -I
authorEnrico Tassi <enrico.tassi@inria.fr>
Fri, 9 Dec 2005 10:52:50 +0000 (10:52 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Fri, 9 Dec 2005 10:52:50 +0000 (10:52 +0000)
helm/matita/matitaScript.ml

index da2c5b2fa168a85080812a7e329004d38f2a2c4d..c14bd77101628212a200e1066d31252c9c9792b5 100644 (file)
@@ -83,6 +83,9 @@ let eval_with_engine guistuff status user_goal parsed_text st =
         | None -> []
         | Some devel -> [MatitamakeLib.root_for_development devel ]
   in
+  let include_ =
+    include_ @ (Helm_registry.get_list Helm_registry.string "matita.includes")
+  in
   let parsed_text_length = String.length parsed_text in
   let loc, ex = 
     match st with TA.Executable (loc,ex) -> loc, ex | _ -> assert false in