chiark / gitweb /
Makefile: Keep the log file after formatting.
authorMark Wooding <mdw@distorted.org.uk>
Fri, 22 Jul 2022 10:20:32 +0000 (11:20 +0100)
committerMark Wooding <mdw@distorted.org.uk>
Fri, 22 Jul 2022 10:20:32 +0000 (11:20 +0100)
Makefile

index a2d9dd3b3f1ea19e0b9d1d2711df444571b91771..eb8ee48eaf6213bd6b5f771a05d70f9e16762899 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -147,7 +147,7 @@ run-latex            = \
        $1 "\def\indexing{y} \nonstopmode \input $<" $(v_null) && \
        makeindex $(v_quiet) -s gind.ist $*.idx $(v_null) && \
        $1 "\def\indexing{n} \nonstopmode \input $<" $(v_null) && \
-       mv $@ ../ && cd ../ && rm -rf t.$@/
+       mv $@ $*.log ../ && cd ../ && rm -rf t.$@/
 clean::; rm -rf t.*/
 
 ## Good old-fashioned DVI.