max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(tests/playground/Makefile): build *.tex by default

Browse source
This commit is contained in:
Sebastian Ullrich 2019-05-29 10:00:44 +02:00
parent adc462789a
commit 423b087782
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/playground/Makefile
View file

@ -32,7 +32,7 @@ CROSS_INPUTS = $(foreach bench,$(CROSS_BENCHES), $(foreach cat, $(CROSS_CATS), $
.SECONDARY: $(LEAN_INPUTS:%=%.out) $(LEAN_INPUTS:%=bench/%.bench) $(CROSS_INPUTS:%=%.out) $(CROSS_INPUTS:%=bench/%.bench)
.DELETE_ON_ERROR:
all: reports report_lean.csv report_cross.csv
all: reports report_lean.tex report_cross.tex
# disable some built-in rules
%.lean: