From: Stefano Zacchiroli Date: Tue, 7 Jan 2003 17:25:59 +0000 (+0000) Subject: - removed no longer used xsl_dir parameter X-Git-Tag: v0_3_99~78 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=820fd1d8c05fcf75c12f635903728cb17abd4576 - removed no longer used xsl_dir parameter --- diff --git a/helm/http_getter/http_getter_env.ml b/helm/http_getter/http_getter_env.ml index f9c789eff..70696c596 100644 --- a/helm/http_getter/http_getter_env.ml +++ b/helm/http_getter/http_getter_env.ml @@ -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); diff --git a/helm/http_getter/http_getter_env.mli b/helm/http_getter/http_getter_env.mli index 9c66f8ff7..7ce96f702 100644 --- a/helm/http_getter/http_getter_env.mli +++ b/helm/http_getter/http_getter_env.mli @@ -36,7 +36,6 @@ val xsl_index : string (* XSLTs' index *) val xml_dir : string (* XMLs' directory *) val rdf_dir : string (* RDFs' directory *) - val xsl_dir : string (* XSLs' directory *) val dtd_dir : string (* DTDs' root directory *) val servers_file : string (* servers.txt file *) val port : int (* port on which getter listens *)