From 024e92b8b3bf29e41ce50004c37d884baa1db847 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 16 Feb 2004 17:21:30 +0000 Subject: [PATCH] - Configuration file moved to /projects/helm/etc. - Configuration file ported to latest version of Helm_registry. --- helm/http_getter/http_getter.conf.xml.sample | 42 ++++++++++++-------- helm/http_getter/main.ml | 2 +- 2 files changed, 27 insertions(+), 17 deletions(-) diff --git a/helm/http_getter/http_getter.conf.xml.sample b/helm/http_getter/http_getter.conf.xml.sample index 01e1f126b..780a05d2e 100644 --- a/helm/http_getter/http_getter.conf.xml.sample +++ b/helm/http_getter/http_getter.conf.xml.sample @@ -1,19 +1,29 @@ - /foo/servers.txt - /foo/cic_library - /foo/nuprl_library - /foo/rdf_library - /foo/dtd - /foo/cic_db - /foo/nuprl_db - /foo/rdf_db - /foo/xsl_db - - gz - index.txt - rdf_index.txt - xslt_index.txt - http://mowgli.cs.unibo.it/dtd - 58081 + /projects/helm/shared/V7_mowgli + /tmp/helm/cache + +
+ $(dbm_dir)/servers.txt + + $(cache_dir)/cic_library + $(cache_dir)/nuprl_library + $(cache_dir)/rdf_library + /projects/helm/xml/dtd + + $(dbm_dir)/cic_db + $(dbm_dir)/nuprl_db + $(dbm_dir)/rdf_db + $(dbm_dir)/xsl_db + + gz + + index.txt + rdf_index.txt + xslt_index.txt + + http://mowgli.cs.unibo.it/dtd + + 38081 +
diff --git a/helm/http_getter/main.ml b/helm/http_getter/main.ml index 90f776df3..7722a2cdc 100644 --- a/helm/http_getter/main.ml +++ b/helm/http_getter/main.ml @@ -35,7 +35,7 @@ open Http_getter_debugger (* constants *) -let configuration_file = "http_getter.conf.xml" +let configuration_file = "/projects/helm/etc/http_getter.conf.xml" let common_headers = [ "Cache-Control", "no-cache"; -- 2.39.2