Makefile: pass --tee option to texfot

Newer versions of texfot put their logging into /tmp/fot.<uid>. Hower, older versions put it in /tmp/fot, which means that if different users use texfot on the same machine, the first one creating the file wins, the other users cannot use fot. In order to work around this, explicitly use /tmp/fot.<uid>. Signed-off-by: Thomas Petazzoni <[email protected]>
bootlin · Aug 7, 2023 · 6b1cbd0 · 6b1cbd0
1 parent 2e001be
commit 6b1cbd0
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Makefile b/Makefile
@@ -31,7 +31,7 @@ VARS = $(OUTDIR)/vars
 
 # Environment for pdflatex, which allows it to find the stylesheet in the
 # common/ directory.
-PDFLATEX_ENV = TEXINPUTS=.:$(shell pwd):$(shell pwd)/common: texfot
+PDFLATEX_ENV = TEXINPUTS=.:$(shell pwd):$(shell pwd)/common: texfot --tee /tmp/fot.`id -u`
 
 # Arguments passed to pdflatex
 PDFLATEX_OPT = -shell-escape -file-line-error -halt-on-error