diff --git a/Doc/fix_libaux.sed b/Doc/fix_libaux.sed
new file mode 100755
index 00000000000..459b7e8d365
--- /dev/null
+++ b/Doc/fix_libaux.sed
@@ -0,0 +1,3 @@
+#! /usr/bin/sed -f
+s/{\\tt  \\hackscore  {}\\hackscore  {}/\\sectcode{__/
+s/\\hackscore  {}\\hackscore  {}/__/
diff --git a/Doc/tools/fix_libaux.sed b/Doc/tools/fix_libaux.sed
new file mode 100755
index 00000000000..459b7e8d365
--- /dev/null
+++ b/Doc/tools/fix_libaux.sed
@@ -0,0 +1,3 @@
+#! /usr/bin/sed -f
+s/{\\tt  \\hackscore  {}\\hackscore  {}/\\sectcode{__/
+s/\\hackscore  {}\\hackscore  {}/__/