From: Luca Padovani Date: Tue, 3 Apr 2001 09:45:18 +0000 (+0000) Subject: added support for HELM_GETTER_URL environment variable X-Git-Tag: v0_1_2~40 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=942fad0fe746ee1f66566664548f84c7c03dcd30;p=helm.git added support for HELM_GETTER_URL environment variable --- diff --git a/helm/interface/configuration.ml.in b/helm/interface/configuration.ml.in index b9358d8ff..d20a3c0c0 100644 --- a/helm/interface/configuration.ml.in +++ b/helm/interface/configuration.ml.in @@ -103,15 +103,15 @@ let read_configuration_var xml_name = let helm_dir = read_configuration_var "helm_dir";; let dtd_dir = read_configuration_var "dtd_dir";; -let style_dir = read_configuration_var_env "style_dir" "HELM_STYLE_DIR" +let style_dir = read_configuration_var_env "style_dir" "HELM_STYLE_DIR";; let servers_file = read_configuration_var "servers_file";; let uris_dbm = read_configuration_var "uris_dbm";; let dest = read_configuration_var "dest";; let indexname = read_configuration_var "indexname";; let tmp_dir = read_configuration_var "tmp_dir" let helm_dir = read_configuration_var "helm_dir";; -let getter_url = read_configuration_var "getter_url";; -let processor_url = read_configuration_var_env "processor_url" "HELM_PROCESSOR_URL" +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 _ = Hashtbl.clear vars;;