From 423b087782065df77f6cdc36c0028e08c7cd3fcc Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 29 May 2019 10:00:44 +0200 Subject: [PATCH] chore(tests/playground/Makefile): build *.tex by default --- tests/playground/Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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: