]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/http_getter/http_getter_env.ml
- removed no longer used xsl_dir parameter
[helm.git] / helm / http_getter / http_getter_env.ml
index f9c789eff50e6d493f34a5bc8757b9c8abad173d..70696c5965f33dee94ced3c6a6a40721f0fee3e2 100644 (file)
@@ -85,7 +85,6 @@ let rdf_index = safe_getenv "HTTP_GETTER_RDF_INDEXNAME"
 let xsl_index = safe_getenv "HTTP_GETTER_XSL_INDEXNAME"
 let xml_dir = safe_getenv "HTTP_GETTER_XML_DIR"
 let rdf_dir = safe_getenv "HTTP_GETTER_RDF_DIR"
-let xsl_dir = safe_getenv "HTTP_GETTER_XSL_DIR"
 let dtd_dir = safe_getenv "HTTP_GETTER_DTD_DIR"
 
 let port =
@@ -121,7 +120,6 @@ rdf_index:\t%s
 xsl_index:\t%s
 xml_dir:\t%s
 rdf_dir:\t%s
-xsl_dir:\t%s
 dtd_dir:\t%s
 servers_file:\t%s
 host:\t\t%s
@@ -135,7 +133,7 @@ servers:
 \t%s
 "
     xml_dbm rdf_dbm xsl_dbm xml_index rdf_index xsl_index
-    xml_dir rdf_dir xsl_dir dtd_dir servers_file host port
+    xml_dir rdf_dir dtd_dir servers_file host port
     my_own_url dtd_base_url
     (match cache_mode with Enc_normal -> "Normal" | Enc_gzipped -> "GZipped")
     conf_file conf_dir (String.concat "\n\t" servers);