from now on, export MATITA_EXTRACT=true to extract

diff --git a/helm/software/matita/matitaInit.ml b/helm/software/matita/matitaInit.ml
index cf96c5ba1261e45a29c0396bd1c1c6778d326016..705108aa659304311e540d12a9e3bb567ad23e48 100644 (file)
--- a/helm/software/matita/matitaInit.ml
+++ b/helm/software/matita/matitaInit.ml
@@ -52,6 +52,7 @@ let registry_defaults = [
   "matita.noinnertypes",         "false";
   "matita.do_heavy_checks",      "true";
   "matita.moo",                  "true";
+  "matita.extract",              "false";
 ]
 
 let set_registry_values =

diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml
index 7470b8febc6ca4670e7b1f821e55dabcc4563c7f..0af97572e11a0dd59e07e5726aea10eab988ad56 100644 (file)
--- a/helm/software/matita/matitacLib.ml
+++ b/helm/software/matita/matitacLib.ml
@@ -110,7 +110,7 @@ let get_include_paths options =
 ;;
 
 let activate_extraction baseuri fname =
- if false then
+ if Helm_registry.get_bool "matita.extract" then
   let mangled_baseuri =
    let baseuri = String.sub baseuri 5 (String.length baseuri - 5) in
      let baseuri = Pcre.replace ~pat:"/" ~templ:"_" baseuri in