from now on, export MATITA_EXTRACT=true to extract

[helm.git] / helm / software / matita / matitaInit.ml

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 =