Makefile: rebuild index if files have been deleted.

Signed-off-by: Daira Hopwood <daira@jacaranda.org>
This commit is contained in:
Daira Hopwood 2020-04-14 13:08:16 +01:00
parent 604532cca1
commit 283480c802
2 changed files with 6 additions and 2 deletions

1
.gitignore vendored
View File

@ -20,6 +20,7 @@
*.save
.Makefile.uptodate
.zipfilelist.*
protocol/aux/
protocol/html/

View File

@ -4,6 +4,9 @@
.PHONY: all all-zips protocol
all-zips: .Makefile.uptodate
find . -name 'zip-*.rst' |sort >.zipfilelist.new
diff .zipfilelist.current .zipfilelist.new || cp -f .zipfilelist.new .zipfilelist.current
rm -f .zipfilelist.new
$(MAKE) README.rst
$(MAKE) index.html $(addsuffix .html,$(filter-out README,$(basename $(wildcard *.rst))))
@ -28,9 +31,9 @@ index.html: README.rst
%.html: %.rst
$(PROCESSRST)
README.rst: makeindex.sh README.template $(wildcard zip-*.rst)
README.rst: .zipfilelist.current makeindex.sh README.template $(wildcard zip-*.rst)
./makeindex.sh | cat README.template - >README.rst
.PHONY: clean
clean:
rm -f README.rst index.html $(addsuffix .html,$(basename $(wildcard *.rst)))
rm -f .zipfilelist.* README.rst index.html $(addsuffix .html,$(basename $(wildcard *.rst)))