]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/http_getter/http_getter.pl.in
Default for patch_dtd modified to "yes".
[helm.git] / 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' ".