From 105a6097411efd3ab1a198426dcf30d9943013e3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 23 May 2007 14:08:27 +0000 Subject: [PATCH] MATITA_* env variable preserved when publishing a development --- helm/software/matita/matitamakeLib.ml | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) 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 -- 2.39.2