Doc/tools/fix_hack - external/github.com/python/cpython - Git at Google

 #!/bin/sh
 sed -e 's/{\\ptt[ 	]*\\char[ 	]*'"'"'137}/_/g' <"$1" > "@$1" && mv "@$1" $1
	#!/bin/sh
	sed -e 's/{\\ptt[ ]\\char[ ]'"'"'137}/_/g' <"$1" > "@$1" && mv "@$1" $1