From: Mark Wooding Date: Thu, 18 May 2023 21:54:13 +0000 (+0100) Subject: Makefile: Delete the log files on `clean'. X-Git-Url: https://www.chiark.greenend.org.uk/ucgi/~mdw/git/mdwtools/commitdiff_plain/3f40da71dd3295d4187f3f82bff4cd0fcda2b9d3 Makefile: Delete the log files on `clean'. --- diff --git a/Makefile b/Makefile index f56e5fd..50a450e 100644 --- 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.