From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 23 May 2007 14:08:27 +0000 (+0000)
Subject: MATITA_* env variable preserved when publishing a development
X-Git-Tag: 0.4.95@7852~460
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=89758b00226ddab59559f144cceeb58f1594b53a;p=helm.git

MATITA_* env variable preserved when publishing a development
---

diff --git a/matita/matitamakeLib.ml b/matita/matitamakeLib.ml
index f811c84e2..4544f9ada 100644
--- a/matita/matitamakeLib.ml
+++ b/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