diff options
Diffstat (limited to 'lispintro/makefile.w32-in')
| -rw-r--r-- | lispintro/makefile.w32-in | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/lispintro/makefile.w32-in b/lispintro/makefile.w32-in index 2131542a110..f7e99334188 100644 --- a/lispintro/makefile.w32-in +++ b/lispintro/makefile.w32-in @@ -39,6 +39,8 @@ ENVADD = $(srcdir)\..\nt\envadd.bat "TEXINPUTS=$(srcdir);$(TEXINPUTS)" \ .SUFFIXES: .dvi .ps .texi info: $(INFO_TARGETS) + +$(infodir)/dir: $(INSTALL_INFO) --info-dir=$(infodir) $(INFO_TARGETS) dvi: $(DVI_TARGETS) |