diff options
Diffstat (limited to 'kdvi/make/texi.make')
| -rw-r--r-- | kdvi/make/texi.make | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/kdvi/make/texi.make b/kdvi/make/texi.make new file mode 100644 index 00000000..ff953cc7 --- /dev/null +++ b/kdvi/make/texi.make @@ -0,0 +1,13 @@ +# texi.make -- making .dvi and .info from .texi. + +MAKEINFO = makeinfo +MAKEINFO_FLAGS = --paragraph-indent=2 -I$(HOME)/gnu/gnuorg +# That -I is purely for my own benefit in doing `make dist'. It won't +# hurt anything for you (I hope). +TEXI2DVI = texi2dvi + +.SUFFIXES: .info .dvi .texi +.texi.info: + -$(MAKEINFO) $(MAKEINFO_FLAGS) $< -o $@ +.texi.dvi: + -$(TEXI2DVI) $(TEXI2DVI_FLAGS) $< |