diff options
| author | Jonas Bernoulli <jonas@bernoul.li> | 2024-08-17 19:18:08 +0200 |
|---|---|---|
| committer | Jonas Bernoulli <jonas@bernoul.li> | 2024-08-17 19:18:08 +0200 |
| commit | 3dcd648fa67e59ee140b5e00ce06bcf55295351e (patch) | |
| tree | cd85e3fd098bf100396132251d0cb13cfe9b8e2d /docs/Makefile | |
| parent | f8a5f7ca50e549988b7e66b8fa5841b0bc33eac3 (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 f50e192..cc8cdde 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) @sed -i -e 's/“/``/g' -e "s/”/''/g" -e '$$a\' $(PKG).texi #' |