DEVTOOLS: Remove vestige of TeX credits encoding

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:
 #