MATITA_* env variable preserved when publishing a development

diff --git a/helm/software/matita/matitamakeLib.ml b/helm/software/matita/matitamakeLib.ml
index f811c84e2ecd56d633a6430d01ae933f62024b6e..4544f9ada5c6f99ebeb23131609b1103d433f584 100644 (file)
--- a/helm/software/matita/matitamakeLib.ml
+++ b/helm/software/matita/matitamakeLib.ml
@@ -325,12 +325,18 @@ let root_for_development development = development.root
 let name_for_development development = development.name
 
 let publish_development_bstract build clean devel = 
-  let matita_flags = "\"-system\"" in
+  let matita_flags, matita_flags_system = 
+    let orig_matita_flags = 
+      try Sys.getenv "MATITA_FLAGS" with Not_found -> "" 
+    in
+    "\"" ^ orig_matita_flags ^ "\"", "\"" ^ orig_matita_flags ^ " -system\"" 
+  in
   HLog.message "cleaning the development before publishing";
-  if clean ~matita_flags:"" devel then
+  if clean ~matita_flags devel then
     begin
       HLog.message "rebuilding the development in 'system' space";
-      if build ~matita_flags devel then
+      (* here we should use pristine metadata if we use sqlite *)
+      if build ~matita_flags:matita_flags_system devel then
         begin
           HLog.message "publishing succeded";
           true