]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/http_getter/http_getter.pl.in
HTTP_GETTER_URIS_DBM added
[helm.git] / helm / http_getter / http_getter.pl.in
index 8a66df336a33fa7734b0c3a38058685dc14e0ff8..f3484d68845d38099360016ebb4e29aec508b74b 100755 (executable)
@@ -66,6 +66,7 @@ my $rdf_indexname = $ENV{'HTTP_GETTER_RDF_INDEXNAME'} ||
 my $xslt_indexname = $ENV{'HTTP_GETTER_XSLT_INDEXNAME'} ||
   "xslt_index.txt";
 $servers_file = $ENV{'HTTP_GETTER_SERVERS_FILE'} || $servers_file;
+$uris_dbm = $ENV{'HTTP_GETTER_URIS_DBM'} || $uris_dbm;
   
 # </move_to_conf_file>