Add html to all (else it is built during install!).

diff --git a/doc/make-common.in b/doc/make-common.in
index 05a384c8fe82c0911db402eeb95017ea45adadb8..319de107c991a952063fd33e5f4e3ed83e2ae1f1 100644 (file)
--- a/doc/make-common.in
+++ b/doc/make-common.in
@@ -75,7 +75,7 @@ PS_TARGET = $(TARGET_ROOT).ps
 
 TEX_OPTIONS = --quiet $(EXTRA_TEX_OPTIONS)
 
-all: $(INFO_TARGET) $(TARGETS)
+all: $(INFO_TARGET) $(HTML_TARGET)/index.html $(TARGETS)
 
 $(INFO_TARGET): $(SOURCES)
        rm -f $(INFO_TARGET)*