From: Claudio Sacerdoti Coen Date: Thu, 22 Nov 2001 13:16:15 +0000 (+0000) Subject: out of sync w.r.t. configuration.ml X-Git-Tag: mlminidom_0_2_2~69 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2c213de9e3012552e9cb2dc07412b1e7be52a69e;p=helm.git out of sync w.r.t. configuration.ml --- diff --git a/helm/metadata/create2/touch/configuration.ml.in b/helm/metadata/create2/touch/configuration.ml.in index d20a3c0c0..c743be135 100644 --- a/helm/metadata/create2/touch/configuration.ml.in +++ b/helm/metadata/create2/touch/configuration.ml.in @@ -112,6 +112,8 @@ let tmp_dir = read_configuration_var "tmp_dir" let helm_dir = read_configuration_var "helm_dir";; let getter_url = read_configuration_var_env "getter_url" "HELM_GETTER_URL";; let processor_url = read_configuration_var_env "processor_url" "HELM_PROCESSOR_URL";; +let annotations_dir = read_configuration_var_env "annotations_dir" "HELM_ANNOTATIONS_DIR" +let annotations_url = read_configuration_var_env "annotations_url" "HELM_ANNOTATIONS_URL" let _ = Hashtbl.clear vars;;