From 1436037fbaeb5155b485371298b3656bc636f22f Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 5 Mar 2008 11:08:21 +0000 Subject: [PATCH] from now on, export MATITA_EXTRACT=true to extract --- helm/software/matita/matitaInit.ml | 1 + helm/software/matita/matitacLib.ml | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/helm/software/matita/matitaInit.ml b/helm/software/matita/matitaInit.ml index cf96c5ba1..705108aa6 100644 --- 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 7470b8feb..0af97572e 100644 --- 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 -- 2.39.2