Do not rebuild html-$(RELEASE).tar every time we need to use it.
diff --git a/Doc/Makefile b/Doc/Makefile
index fce0848..1e51903 100644
--- a/Doc/Makefile
+++ b/Doc/Makefile
@@ -367,7 +367,7 @@
 	rm -f $@
 	cd paper-$(PAPER) && zip -q -9 ../$@ *.ps README
 
-html-$(RELEASE).tar:	html
+html-$(RELEASE).tar:	$(ALLHTMLFILES)
 	cd $(HTMLDIR) && \
 		tar cf ../html-$(RELEASE).tar *.html */*.css */*.html \
 					      */*.gif */*.txt