From: Stefano Zacchiroli Date: Wed, 27 Jun 2001 09:14:34 +0000 (+0000) Subject: added support for new environment variables X-Git-Tag: v0_1_3~129 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0c10a9daa0571da2621b2d8ced0434021d114f8c;p=helm.git added support for new environment variables - HTTP_GETTER_RDF_DIR, cache dir for rdf metadata - HTTP_GETTER_RDF_DBM, dbm file that map rdf uri to url _without_ .db ext - HTTP_GETTER_RDF_INDEXNAME, name of the indexfile that contain rdf index --- diff --git a/helm/http_getter/configure.in b/helm/http_getter/configure.in index eef0bcf32..d8325a743 100644 --- a/helm/http_getter/configure.in +++ b/helm/http_getter/configure.in @@ -3,7 +3,7 @@ AC_INIT(http_getter.pl.in) PACKAGE=helm_http_getter MAJOR_VERSION=0 MINOR_VERSION=1 -MICRO_VERSION=48 +MICRO_VERSION=49 VERSION=$MAJOR_VERSION.$MINOR_VERSION.$MICRO_VERSION DEFAULT_HELM_LIB_DIR=/usr/local/lib/helm diff --git a/helm/http_getter/http_getter.pl.in b/helm/http_getter/http_getter.pl.in index 9c71fce07..6c6a7340e 100755 --- a/helm/http_getter/http_getter.pl.in +++ b/helm/http_getter/http_getter.pl.in @@ -43,23 +43,23 @@ if (defined ($HELM_LIB_DIR)) { $HELM_LIB_PATH = $DEFAULT_HELM_LIB_DIR."/configuration.pl"; } -# : TODO temporary, move this setting to configuration file -# set the cache mode, may be "gzipped" or "normal" -my $cachemode = $ENV{'HTTP_GETTER_CACHE_MODE'} || 'gzipped'; -if (($cachemode ne 'gzipped') and ($cachemode ne 'normal')) { - die "Invalid HTTP_GETTER_CACHE_MODE environment variable, must be". - "'normal' or 'gzipped'\n"; -} -# - # next require defines: $helm_dir, $html_link, $dtd_dir, $uris_dbm, $indexname require $HELM_LIB_PATH; # TEMP: TODO put these vars in configuration file configuration.xml # -$helm_rdf_dir = "/usr/local/helm/rdf_library"; -$rdf_dbm = "/usr/local/helm/rdf_urls_of_uris"; -$rdf_indexname = "rdf_index.txt"; +my $cachemode = $ENV{'HTTP_GETTER_CACHE_MODE'} || + 'gzipped'; +if (($cachemode ne 'gzipped') and ($cachemode ne 'normal')) { + die "Invalid HTTP_GETTER_CACHE_MODE environment variable, must be". + "'normal' or 'gzipped'\n"; +} +my $helm_rdf_dir = $ENV{'HTTP_GETTER_RDF_DIR'} || + "/usr/local/helm/rdf_library"; +my $rdf_dbm = $ENV{'HTTP_GETTER_RDF_DBM'} || + "/usr/local/helm/rdf_urls_of_uris"; +my $rdf_indexname = $ENV{'HTTP_GETTER_RDF_INDEXNAME'} || + "rdf_index.txt"; # # Let's override the configuration file @@ -595,7 +595,7 @@ sub download { my ($gz, $buffer); # print "DOWNLOAD subs receives url: \"$url\"\n"; -$ print "DOWNLOAD subs receives filename: \"$filename\"\n"; +# print "DOWNLOAD subs receives filename: \"$filename\"\n"; my $resourcetype; # retrieve mode: "normal" (.xml) or "gzipped" (.xml.gz) if ($filename =~ /\.xml$/) { # set retrieve mode