]> matita.cs.unibo.it Git - helm.git/commitdiff
removed tmp_dir no longer needed (it was used only by ClientHTTP module)
authorStefano Zacchiroli <zack@upsilon.cc>
Wed, 19 Feb 2003 14:29:18 +0000 (14:29 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Wed, 19 Feb 2003 14:29:18 +0000 (14:29 +0000)
helm/ocaml/getter/configuration.ml
helm/ocaml/getter/configuration.mli

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"
index 3dae0e000f388db2223a6c270cdaa91d7c028cc2..20daaa411c34b571f99b3c2ca7f968606ac7df16 100644 (file)
@@ -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