Move latex-generation into build with latexmk used if available

Author: mn200

examples/latex-generation/paper/Holmakefile

@@ -1,16 +1,20 @@
 INCLUDES = ../theories
 
+LATEXMK_EXISTS = $(if $(which latexmk),yes,no)
+
+ifeq($(LATEXMK_EXISTS), yes)
 paper.pdf: paper.tex holtexbasic.sty
 	latexmk -pdf paper
-
-munge: ppLib.uo
-	$(HOLDIR)/bin/mkmunge.exe -o $@ $<
+endif
 
 paper.tex: paper.htex overrides munge
 	./munge overrides < $< > $@
 
+munge: ppLib.uo
+	$(HOLDIR)/bin/mkmunge.exe -o $@ $<
 
 holtexbasic.sty: $(HOLDIR)/src/TeX/holtexbasic.sty
 	$(CP) $< $@
 
-EXTRA_CLEANS = holtexbasic.sty paper.pdf paper.tex paper.fls paper.aux paper.fdb_latexmk paper.log munge
+EXTRA_CLEANS = holtexbasic.sty paper.pdf paper.tex paper.fls paper.aux \
+               paper.fdb_latexmk paper.log munge

src/parallel_builds/core/Holmakefile

@@ -52,7 +52,7 @@ EXDIRS = algebra/aat \
          hardware hfs \
          imperative ind_def \
          l3-machine-code/common \
-         lambda \
+         lambda latex-generation/paper \
          logic logic/folcompactness logic/modal-models logic/modal-tableaux \
          logic/ncfolproofs logic/propositional_logic logic/relevant-logic \
          logic/temporal/src \