]> matita.cs.unibo.it Git - helm.git/commitdiff
bug fix in configuration dependences
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Fri, 21 Sep 2007 20:47:15 +0000 (20:47 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Fri, 21 Sep 2007 20:47:15 +0000 (20:47 +0000)
matita/matitaInit.ml

index 26f4b40ffe421a1867b85e6358137ea5730ae187..cf821c1673b20fe5b7ab073af17df7d05c3a3778 100644 (file)
@@ -112,7 +112,7 @@ let initialize_makelib init_status =
     init_status
 
 let initialize_environment init_status = 
-  wants [ConfigurationFile] init_status;
+  wants [CmdLine] init_status;
   if not (already_configured [Getter;Environment] init_status) then
     begin
       Http_getter.init ();