diff options
| -rw-r--r-- | Doc/Makefile | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/Doc/Makefile b/Doc/Makefile index 8c2c4ed..49608da 100644 --- a/Doc/Makefile +++ b/Doc/Makefile @@ -166,7 +166,8 @@ include Makefile.deps # Main target -all: html +default: html +all: html dvi ps pdf isilo dvi: $(DVIFILES) pdf: $(PDFFILES) |