- removed no longer used xsl_dir parameter

[helm.git] / helm / http_getter / http_getter_env.mli

diff --git a/helm/http_getter/http_getter_env.mli b/helm/http_getter/http_getter_env.mli
index 9c66f8ff7a0dd18f2844c358527b079044ce33de..7ce96f70220d929bb87953344a4adf475df49963 100644 (file)
--- 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 *)