]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/matitacLib.ml
new apply almost there
[helm.git] / helm / software / matita / matitacLib.ml
index cfec1c5072512ace47dd29b2ef4ef505d48f1959..e793a725b61b3019c81ca31242729ce5c1d5d4f8 100644 (file)
@@ -193,11 +193,11 @@ let compile options fname =
     Librarian.baseuri_of_script ~include_paths fname in
   if Http_getter_storage.is_read_only baseuri then assert false;
   activate_extraction baseuri fname ;
-  let grafite_status = GrafiteSync.init baseuri in
   let lexicon_status = 
     CicNotation2.load_notation ~include_paths:[]
       BuildTimeConf.core_notation_script 
   in
+  let grafite_status = GrafiteSync.init lexicon_status baseuri in
   let big_bang = Unix.gettimeofday () in
   let { Unix.tms_utime = big_bang_u ; Unix.tms_stime = big_bang_s} = 
     Unix.times ()