diff options
| -rwxr-xr-x | Doc/tools/fix_libaux.sed | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Doc/tools/fix_libaux.sed b/Doc/tools/fix_libaux.sed index 459b7e8..fb33cc5 100755 --- a/Doc/tools/fix_libaux.sed +++ b/Doc/tools/fix_libaux.sed @@ -1,3 +1,3 @@ -#! /usr/bin/sed -f +#! /bin/sed -f s/{\\tt \\hackscore {}\\hackscore {}/\\sectcode{__/ s/\\hackscore {}\\hackscore {}/__/ |