diff options
Diffstat (limited to 'gnu')
| -rwxr-xr-x | gnu/dist/texinfo/util/texi2dvi | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/gnu/dist/texinfo/util/texi2dvi b/gnu/dist/texinfo/util/texi2dvi index 4722f152a5e..9e4d3c5eb0f 100755 --- a/gnu/dist/texinfo/util/texi2dvi +++ b/gnu/dist/texinfo/util/texi2dvi @@ -605,10 +605,10 @@ $textra" "$filename_input" >"$filename_xtr" # If this is a Texinfo file with a specified input encoding, and # recode is available, then recode to plain 7 bit Texinfo. if test $language = texinfo; then - pgm='s/\(^\|.* \)@documentencoding *\([^ ][^ ]*\)\( .*\|$\)/\2/ - t found - d - :found + pgm='s/\(^\|.* \)@documentencoding *\([^ ][^ ]*\)\( .*\|$\)/\2/ + t found + d + :found q' encoding=`sed -e "$pgm" "$filename_input"` if $recode && test -n "$encoding" && findprog recode; then |
