]> matita.cs.unibo.it Git - helm.git/commitdiff
- added support for file ls (i.e. you can use a baseuri that point to a
authorStefano Zacchiroli <zack@upsilon.cc>
Tue, 20 Mar 2001 17:30:32 +0000 (17:30 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Tue, 20 Mar 2001 17:30:32 +0000 (17:30 +0000)
  file with ls)
- change the installcgi method in Makefile, now no error if no cgi is
  going to be installed

helm/http_getter/Makefile.in
helm/http_getter/http_getter.pl.in

index 602c8d36208c353b3e208c50e1638682ca7fee0f..f4e6b592d144161cb9a4844aabd8916a5064d0f8 100644 (file)
@@ -11,13 +11,19 @@ installgetter:
        cp http_getter.pl $(INSTALL_DIR)/
 
 installcgi:
-       cp *.cgi $(CGI_DIR)/
+       for f in *.cgi; do \
+  if [ -f $$f ]; then \
+   cp -f $$f $(CGI_DIR)/; \
+  fi; \
+ done
 
 uninstallgetter:
        rm $(INSTALL_DIR)/http_getter.pl
 
 uninstallcgi:
-       for f in *.cgi; do rm -f $(CGI_DIR)/$$f; done
+       for f in *.cgi; do \
+  rm -f $(CGI_DIR)/$$f; \
+ done
 
 clean:
 
index e301963bcf65af3225a866a54c5a82306fc4cfdd..924ddbb1930e966ef1c810e5f1633d597e31ca44 100755 (executable)
@@ -311,21 +311,32 @@ sub finduris { # find uris for cic and theory trees generation
  my ($uri,$localpart,$basepart,$dirname,$suffix,$flags,$key);
  my (@itemz,@already_pushed_dir);
  my (%objects,%dirs); # map uris to suffixes' flags
+ #my $debug=1; # for debug
 
  print "FINDURIS, uritype: $uritype, uripattern: $uripattern, ".
-  "format: $format\n\n";
+  "format: $format\n\n" if defined($debug);
  
  if (($uritype eq "cic") or ($uritype eq "theory")) {
    # get info only of one type: cic or theory
   foreach (keys(%map)) { # select matching uris
    $uri = $_;
-   if ($uri =~ /^$uritype:$uripattern\//) {
-    $localpart = $uri;
-    $localpart =~ s/^$uritype:$uripattern\/(.*)/$1/;
+   if ($uri =~ /^$uritype:$uripattern(\/|$|\.)/) {
+    if ($uri =~ /^$uritype:$uripattern\//) { # directory match
+     $localpart = $uri;
+     $localpart =~ s/^$uritype:$uripattern\/(.*)/$1/;
+    } elsif ($uri =~ /^$uritype:$uripattern($|\.)/) { # file match
+     $localpart = $uri;
+     $localpart =~ s/^.*\/([^\/]*)/$1/;
+    } else {
+     die "Internal error, seems that requested match is none of ".
+      "directory match or file match";
+    }
+    print "LOCALPART: $localpart\n" if defined($debug);
 
     if ($localpart =~ /^[^\/]*$/) { # no slash, an OBJECT
      $basepart = $localpart;
-     $basepart =~ s/^([^.]*\.[^.]*)(\.types)?(\.ann)?/$1/; # remove exts .types or
+     $basepart =~ s/^([^.]*\.[^.]*)(\.types)?(\.ann)?/$1/;
+                                              # remove exts .types or
                                               # .types.ann
      $flags = $objects{$basepart}; # get old flags
      if ($localpart =~ /\.ann$/) {