diff --git a/tests/playground/Makefile b/tests/playground/Makefile index a05adc3670..7ffd201a17 100644 --- a/tests/playground/Makefile +++ b/tests/playground/Makefile @@ -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: