chiark / gitweb /
Makefile: Delete the log files on `clean'.
authorMark Wooding <mdw@distorted.org.uk>
Thu, 18 May 2023 21:54:13 +0000 (22:54 +0100)
committerMark Wooding <mdw@distorted.org.uk>
Thu, 18 May 2023 21:54:13 +0000 (22:54 +0100)
Makefile

index f56e5fd28a72d574b5b7ba4d15a109ab5b256624..50a450e9d0db7e3921aa89b6dcc727940ce24949 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -149,6 +149,7 @@ makeindex $(v_quiet) -s gind.ist $*.idx $(v_null) && \
 $1 "\def\indexing{n} \nonstopmode \input $<" $(v_null) && \
 mv $@ $*.log ../ && cd ../ && rm -rf t.$@/
 endef
+CLEANFILES             += *.log
 clean::; rm -rf t.*/
 
 ## Good old-fashioned DVI.