]> matita.cs.unibo.it Git - helm.git/commitdiff
Format of rdf URIs relaxed
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 26 Jun 2001 15:58:21 +0000 (15:58 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 26 Jun 2001 15:58:21 +0000 (15:58 +0000)
helm/http_getter/http_getter.pl.in

index 40fd3118d1b1b156635587bbb49e6eaf8e4a03bf..3e0db46dbdb24f961b39553a585039daf3cddd86 100755 (executable)
@@ -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;