]> matita.cs.unibo.it Git - helm.git/commitdiff
Default for patch_dtd modified to "yes".
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 11 Jun 2001 13:37:56 +0000 (13:37 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 11 Jun 2001 13:37:56 +0000 (13:37 +0000)
helm/http_getter/http_getter.pl.in

index e06a3a5e2fbd43e6d3f8cc93bfed0131164d3062..7017d1957685876580f6dec934da45237a27a61a 100755 (executable)
@@ -113,7 +113,7 @@ while (my $c = $d->accept) {
             my $answerformat = $cgi->param('format');
             my $patch_dtd = $cgi->param('patch_dtd');
             $answerformat = "" if (not defined($answerformat));
-            $patch_dtd = "" if (not defined($patch_dtd));
+            $patch_dtd = "yes" if (not defined($patch_dtd));
             if (($answerformat ne "gz") and ($answerformat ne "normal")
                and ($answerformat ne "")) {
              die "Wrong output format: $answerformat, must be 'normal' ".