From: Enrico Tassi Date: Wed, 23 May 2007 14:08:27 +0000 (+0000) Subject: MATITA_* env variable preserved when publishing a development X-Git-Tag: make_still_working~6319 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=105a6097411efd3ab1a198426dcf30d9943013e3;p=helm.git MATITA_* env variable preserved when publishing a development --- diff --git a/helm/software/matita/matitamakeLib.ml b/helm/software/matita/matitamakeLib.ml index f811c84e2..4544f9ada 100644 --- 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