diff options
-rw-r--r-- | Doc/html/Makefile | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/Doc/html/Makefile b/Doc/html/Makefile index 5da7cab..4cd8423 100644 --- a/Doc/html/Makefile +++ b/Doc/html/Makefile @@ -77,7 +77,6 @@ doc/doc.html: $(DOCFILES) $(BUILDINDEX) $(MKHTML) $(TOPDIR)/doc/doc.tex ext/ext.html: $(EXTFILES) - echo $(EXTFILES) $(MKHTML) $(TOPDIR)/ext/ext.tex lib/lib.html: $(LIBFILES) $(BUILDINDEX) |