From: wolf Date: Mon, 4 Apr 2005 19:30:17 +0000 (+0000) Subject: Use proper quotation marks. X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=91b421d842cfb1f8251d49f9c85c2e99352b0481;p=dealii-svn.git Use proper quotation marks. git-svn-id: https://svn.dealii.org/trunk@10350 0785d39b-7218-0410-832d-ea1e28bc413d --- diff --git a/deal.II/doc/tutorial/chapter-2.step-by-step/program2toc b/deal.II/doc/tutorial/chapter-2.step-by-step/program2toc index 26b94bd426..b3de80eb47 100644 --- a/deal.II/doc/tutorial/chapter-2.step-by-step/program2toc +++ b/deal.II/doc/tutorial/chapter-2.step-by-step/program2toc @@ -6,6 +6,10 @@ while (<>) { $newlevel = $1; $text = $2; + # replace quotation marks by the appropriate HTML quotation marks + $text =~ s!``!“!g; + $text =~ s!''!”!g; + # only allow header levels 3 and 4, since higher ones are # reserved for top-level document headers if (! ($newlevel =~ /[34]/)) {