From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 26 Jun 2001 15:58:21 +0000 (+0000)
Subject: Format of rdf URIs relaxed
X-Git-Tag: v0_1_3~132
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d967a8607248901371c32efdd510e3d1fe353bd5;p=helm.git

Format of rdf URIs relaxed
---

diff --git a/helm/http_getter/http_getter.pl.in b/helm/http_getter/http_getter.pl.in
index 40fd3118d..3e0db46db 100755
--- a/helm/http_getter/http_getter.pl.in
+++ b/helm/http_getter/http_getter.pl.in
@@ -57,8 +57,8 @@ require $HELM_LIB_PATH;
 
 # TEMP: TODO put these vars in configuration file configuration.xml
 # <move_to_conf_file>
-$helm_rdf_dir = "/usr/local/helm/rdf";
-$rdf_dbm = "/usr/local/helm/rdf_urls";
+$helm_rdf_dir = "/projects/helm/shared/V7/rdf_library";
+$rdf_dbm = "/projects/helm/shared/V7/rdf_urls_of_uris";
 $rdf_indexname = "rdf_index.txt";
 # </move_to_conf_file>
 
@@ -369,7 +369,7 @@ sub isRdfUri { # return true if the uri is an rdf uri, false otherwise
 # the format is "helm:rdf/<metadata_tree>:<metadata_scheme>//<xml_file_uri>"
 #
  my ($uri) = @_;
- if ($uri =~ /^helm:rdf(.*):?(.*)\/\/(.*)/) {
+ if ($uri =~ /^helm:rdf(.*):(.*)\/\/(.*)/) {
   return 1;
  } else {
   return 0;