diff --git a/Doc/tools/fix_libaux.sed b/Doc/tools/fix_libaux.sed index 459b7e8d365..fb33cc575de 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 {}/__/