]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/cgi/mkindextheory.pl
getter flags considered
[helm.git] / helm / cgi / mkindextheory.pl
index 05bb5b925bf91fbc48255c9c25b0ef4afe79373b..b92f363611f6437db70f20e4eeb12ad84fe6e3cd 100755 (executable)
@@ -44,7 +44,10 @@ EOT
 }
 
 foreach $i (@filenames) {
-   my ($type,$name) = split(/,/, $i);
+   my ($type,$name,$flags) = split(/, /, $i);
+   my ($flagscic, $flagstypes) = split(/,/, $flags);
+   $flagscic =~ s/^<(.*)/$1/;
+   $flagstypes =~ s/(.*)>$/$1/;
    if ($type eq "dir") {
       $output .= <<EOT;
 <tr>
@@ -58,7 +61,7 @@ EOT
            $output .= <<EOT;
 <tr>
 <td><img border="0" src="/icons/generic.red.gif" alt="[DIR]"></td>
-<td><a href="" target="theory" onClick="this.href=makeURL('theory','$uri$name','$processor_url','$getter_url')" onMouseOver="window.status='$uri$name'; return true">$name</a>
+<td><a href="" target="theory" onClick="this.href=makeURL('theory','$uri$name','$processor_url','$getter_url','$flagscic','$flagstypes')" onMouseOver="window.status='$uri$name'; return true">$name</a>
 </tr>
 EOT
          } else {