Added utility target tarhtml to tar and gzip the HTML files plus their
support (GIFS, icons, style sheets).
diff --git a/Doc/Makefile b/Doc/Makefile
index 468294d..e0d48c3 100644
--- a/Doc/Makefile
+++ b/Doc/Makefile
@@ -199,6 +199,10 @@
 	mv api/xxx api/api.html
 	ln -s api.html api/index.html || true
 
+tarhtml: l2h
+	@echo "Did you remember to run makeMIFs.py in the ref subdirectory...?"
+	tar cf - index.html ???/???.css ???/*.html lib/*.gif icons/*.* | gzip >html.tar.gz
+
 
 # Housekeeping targets