From: Claudio Sacerdoti Coen Date: Mon, 11 Jun 2001 13:37:56 +0000 (+0000) Subject: Default for patch_dtd modified to "yes". X-Git-Tag: v0_1_3~151 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2d725daf9ffb06f2f33fe28065703905a9003d23;p=helm.git Default for patch_dtd modified to "yes". --- diff --git a/helm/http_getter/http_getter.pl.in b/helm/http_getter/http_getter.pl.in index e06a3a5e2..7017d1957 100755 --- a/helm/http_getter/http_getter.pl.in +++ b/helm/http_getter/http_getter.pl.in @@ -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' ".