]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/getter/configuration.ml
removed tmp_dir no longer needed (it was used only by ClientHTTP module)
[helm.git] / helm / ocaml / getter / configuration.ml
index 16dc9d0f585aed1d27cd28384849c54ff6210c33..d5fd0e40f5c29647bdf83a97a42eb61eca706d78 100644 (file)
@@ -104,7 +104,8 @@ let read_configuration_var xml_name =
    flush stdout ;
    raise Not_found
 
-let tmp_dir       = read_configuration_var_env "tmp_dir" "HELM_TMP_DIR";;
+(* Zack: no longer used *)
+(* let tmp_dir       = read_configuration_var_env "tmp_dir" "HELM_TMP_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"