commit bb63b7ced72a016967e55726624e149a692486cb parent 91c82fc754d54154e8eb4085b646faf4b62325a9 Author: Wolfgang Corcoran-Mathe <wcm@sigwinch.xyz> Date: Fri, 2 Feb 2024 12:39:26 -0500 Makefile: Allow makeinfo options to be customized; remove PHONY. Diffstat:
| M | doc/r7rs-small/Makefile | | | 11 | ++++++----- |
1 file changed, 6 insertions(+), 5 deletions(-)
diff --git a/doc/r7rs-small/Makefile b/doc/r7rs-small/Makefile @@ -1,12 +1,13 @@ -.PHONY: all +MAKEINFO = makeinfo +MAKEINFOFLAGS = --no-split + all: r7rs-small.html r7rs-small.info r7rs-small.pdf - printf '' r7rs-small.html: r7rs-small.texinfo - makeinfo --html --no-split $< + $(MAKEINFO) $(MAKEINFOFLAGS) --html $< r7rs-small.info: r7rs-small.texinfo - makeinfo --info --no-split $< + $(MAKEINFO) $(MAKEINFOFLAGS) --info $< r7rs-small.pdf: r7rs-small.texinfo - makeinfo --pdf --no-split $< + $(MAKEINFO) $(MAKEINFOFLAGS) --pdf $<