]> matita.cs.unibo.it Git - helm.git/commitdiff
- removed no longer used xsl_dir parameter
authorStefano Zacchiroli <zack@upsilon.cc>
Tue, 7 Jan 2003 17:25:59 +0000 (17:25 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Tue, 7 Jan 2003 17:25:59 +0000 (17:25 +0000)
helm/http_getter/http_getter_env.ml
helm/http_getter/http_getter_env.mli

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);
index 9c66f8ff7a0dd18f2844c358527b079044ce33de..7ce96f70220d929bb87953344a4adf475df49963 100644 (file)
@@ -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 *)