]> matita.cs.unibo.it Git - helm.git/commitdiff
added support for HELM_GETTER_URL environment variable
authorLuca Padovani <luca.padovani@unito.it>
Tue, 3 Apr 2001 09:45:18 +0000 (09:45 +0000)
committerLuca Padovani <luca.padovani@unito.it>
Tue, 3 Apr 2001 09:45:18 +0000 (09:45 +0000)
helm/interface/configuration.ml.in

index b9358d8ff645283e98b2948150df28999d22d31b..d20a3c0c0e0cf872dcb42de6cd4ccdbacad15803 100644 (file)
@@ -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;;