diff options
Diffstat (limited to 'Doc/tools/fix_libaux.sed')
| -rwxr-xr-x | Doc/tools/fix_libaux.sed | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/Doc/tools/fix_libaux.sed b/Doc/tools/fix_libaux.sed deleted file mode 100755 index fb33cc5..0000000 --- a/Doc/tools/fix_libaux.sed +++ /dev/null @@ -1,3 +0,0 @@ -#! /bin/sed -f -s/{\\tt \\hackscore {}\\hackscore {}/\\sectcode{__/ -s/\\hackscore {}\\hackscore {}/__/ |