diff options
| -rw-r--r-- | man/makefile.w32-in | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/man/makefile.w32-in b/man/makefile.w32-in index 09f314dbf47..241d50be956 100644 --- a/man/makefile.w32-in +++ b/man/makefile.w32-in | |||
| @@ -125,9 +125,11 @@ dvi: $(DVI_TARGETS) | |||
| 125 | # The following target uses an explicit -o switch to work around | 125 | # The following target uses an explicit -o switch to work around |
| 126 | # the @setfilename directive in info.texi, which is required for | 126 | # the @setfilename directive in info.texi, which is required for |
| 127 | # the Texinfo distribution. | 127 | # the Texinfo distribution. |
| 128 | # Some Windows ports of makeinfo seem to require -o to come before the | ||
| 129 | # texi filename, contrary to GNU standards. | ||
| 128 | 130 | ||
| 129 | $(infodir)/info: $(INFOSOURCES) | 131 | $(infodir)/info: $(INFOSOURCES) |
| 130 | $(MAKEINFO) --no-split info.texi -o $@ | 132 | $(MAKEINFO) --no-split -o $@ info.texi |
| 131 | 133 | ||
| 132 | info.dvi: $(INFOSOURCES) | 134 | info.dvi: $(INFOSOURCES) |
| 133 | $(ENVADD) $(TEXI2DVI) $(srcdir)/info.texi | 135 | $(ENVADD) $(TEXI2DVI) $(srcdir)/info.texi |