From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Wed, 19 Feb 2003 14:29:18 +0000 (+0000)
Subject: removed tmp_dir no longer needed (it was used only by ClientHTTP module)
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=d85b0968d751d57274b253f1fcf239aa171b8e69

removed tmp_dir no longer needed (it was used only by ClientHTTP module)
---

diff --git a/helm/ocaml/getter/configuration.ml b/helm/ocaml/getter/configuration.ml
index 16dc9d0f5..d5fd0e40f 100644
--- a/helm/ocaml/getter/configuration.ml
+++ b/helm/ocaml/getter/configuration.ml
@@ -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"
diff --git a/helm/ocaml/getter/configuration.mli b/helm/ocaml/getter/configuration.mli
index 3dae0e000..20daaa411 100644
--- a/helm/ocaml/getter/configuration.mli
+++ b/helm/ocaml/getter/configuration.mli
@@ -33,7 +33,8 @@
 (*                                                                            *)
 (******************************************************************************)
 
-val tmp_dir : string
+(* Zack: no longer needed *)
+(* val tmp_dir : string *)
 val getter_url : string
 val processor_url : string
 val annotations_dir : string