diff options
-rwxr-xr-x | devtools/credits.pl | 25 |
1 files changed, 0 insertions, 25 deletions
diff --git a/devtools/credits.pl b/devtools/credits.pl index 68a014deab..0cbd549f74 100755 --- a/devtools/credits.pl +++ b/devtools/credits.pl @@ -155,31 +155,6 @@ sub html_entities_to_rtf { return $text; } -# Convert HTML entities to TeX codes -sub html_entities_to_tex { - my $text = shift; - - $text =~ s/á/\\'a/g; - $text =~ s/é/\\'e/g; - $text =~ s/í/\\'i/g; - $text =~ s/ì/\\`\\i/g; - $text =~ s/ó/\\'o/g; - $text =~ s/ø/{\\o}/g; - $text =~ s/å/\\aa /g; - $text =~ s/ł/{\\l}/g; - $text =~ s/Š/{\\v S}/g; - $text =~ s/ñ/\\˜n/g; - - $text =~ s/ä/\\"a/g; - $text =~ s/ö/\\"o/g; - $text =~ s/ë/\\"e/g; - $text =~ s/ü/\\"u/g; - - $text =~ s/&/\\&/g; - - return $text; -} - # # Small reference of the RTF commands used here: # |