diff options
Diffstat (limited to 'Doc/tools/fix_hack')
| -rwxr-xr-x | Doc/tools/fix_hack | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/Doc/tools/fix_hack b/Doc/tools/fix_hack index 8c97729..8dad111 100755 --- a/Doc/tools/fix_hack +++ b/Doc/tools/fix_hack @@ -1 +1,2 @@ +#!/bin/sh sed -e 's/{\\ptt[ ]*\\char[ ]*'"'"'137}/_/g' <"$1" > "@$1" && mv "@$1" $1 |