diff options
| author | Jonas Bernoulli <jonas@bernoul.li> | 2024-08-17 19:18:19 +0200 |
|---|---|---|
| committer | Jonas Bernoulli <jonas@bernoul.li> | 2024-08-17 19:18:19 +0200 |
| commit | 1380f7c4887e4f956a648baa33d4e05c419169ce (patch) | |
| tree | f6691f22971fea316cc5dc7ecae2df16ecd56699 /docs/Makefile | |
| parent | 4fa6c31c8f8e3fb5536334bac9d62b652dfb5634 (diff) | |
make: Re-generate %.texi if HEAD changed since previous run
Diffstat (limited to 'docs/Makefile')
| -rw-r--r-- | docs/Makefile | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/docs/Makefile b/docs/Makefile index 7a39da8..4285014 100644 --- a/docs/Makefile +++ b/docs/Makefile @@ -18,7 +18,11 @@ redo-docs: @touch $(PKG).org @make docs -%.texi: %.org +.revdesc: ; +_ := $(shell test "$(REVDESC)" = "$$(cat .revdesc 2> /dev/null)" ||\ + echo "$(REVDESC)" > .revdesc) + +%.texi: %.org .revdesc @printf "Generating $@\n" @$(EMACS) $(ORG_ARGS) $< $(ORG_EVAL) |