Incorporated Jan-Hein's changes and texinfo conversion.
diff --git a/Doc/tools/fix_hack b/Doc/tools/fix_hack
new file mode 100755
index 0000000..8c97729
--- /dev/null
+++ b/Doc/tools/fix_hack
@@ -0,0 +1 @@
+sed -e 's/{\\ptt[ 	]*\\char[ 	]*'"'"'137}/_/g' <"$1" > "@$1" && mv "@$1" $1