From f8407b2f84107d8c5a47ce057f1615ea2afa636f Mon Sep 17 00:00:00 2001 From: Matt Birkholz Date: Tue, 12 Jun 2018 16:41:09 -0700 Subject: [PATCH] Add html to all (else it is built during install!). --- doc/make-common.in | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/make-common.in b/doc/make-common.in index 05a384c8f..319de107c 100644 --- 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)* -- 2.25.1