diff options
| -rw-r--r-- | doc/misc/Makefile.in | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/doc/misc/Makefile.in b/doc/misc/Makefile.in index f1dbf3bcc08..c657551862b 100644 --- a/doc/misc/Makefile.in +++ b/doc/misc/Makefile.in @@ -209,6 +209,12 @@ mkinfodir = @cd ${srcdir}; test -d ${infodir} || mkdir ${infodir} || test -d ${i info: $(INFO_TARGETS) +webhack: clean + echo '@set WEBHACKDEVEL' > overrides.texi + +nowebhack: clean + echo '@clear WEBHACKDEVEL' > overrides.texi + dvi: $(DVI_TARGETS) pdf: $(PDF_TARGETS) |