initial source import
diff --git a/doc/tools/fix_hack b/doc/tools/fix_hack
new file mode 100755
index 0000000..8dad111
--- /dev/null
+++ b/doc/tools/fix_hack
@@ -0,0 +1,2 @@
+#!/bin/sh
+sed -e 's/{\\ptt[ 	]*\\char[ 	]*'"'"'137}/_/g' <"$1" > "@$1" && mv "@$1" $1