diff options
Diffstat (limited to 'msdos/sed6.inp')
-rw-r--r-- | msdos/sed6.inp | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/msdos/sed6.inp b/msdos/sed6.inp index 6d44f995307..22052140b82 100644 --- a/msdos/sed6.inp +++ b/msdos/sed6.inp @@ -19,6 +19,8 @@ /^srcdir *=/s/@[^@\n]*@/./ /^VPATH *=/s/@[^@\n]*@/./ /^MAKEINFO *=/s/@[^@\n]*@/makeinfo/ +/^INFO_EXT *=/s/@[^@\n]*@/.info/ +/^INFO_OPTS *=/s/@[^@\n]*@/--no-split/ /^ENVADD/,/^$/c\ ENVADD =\ export TEXINPUTS := $(srcdir)";"$(TEXINPUTS)\ |