From 820fd1d8c05fcf75c12f635903728cb17abd4576 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Tue, 7 Jan 2003 17:25:59 +0000 Subject: [PATCH] - removed no longer used xsl_dir parameter --- helm/http_getter/http_getter_env.ml | 4 +--- helm/http_getter/http_getter_env.mli | 1 - 2 files changed, 1 insertion(+), 4 deletions(-) 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 *) -- 2.39.2