From c0a6916549b55fbae2226e4c34af45e500928645 Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Fri, 24 May 2024 14:56:26 +0200
Subject: Fix running individual tests

---
 Makefile | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index b3dc9f2b..ca3bd66c 100644
--- a/Makefile
+++ b/Makefile
@@ -47,7 +47,12 @@ build-test-verify: build test verify
 
 # Build the project, without formatting the code
 .PHONY: build-dev
+ifdef IN_CI
+build-dev:
+	@true
+else
 build-dev: build-bin build-lib build-bin-dir doc
+endif
 
 .PHONY: build-bin
 build-bin: check-charon
@@ -166,14 +171,13 @@ test-all: $(INPUTS_LIST)
 ifdef IN_CI
 # In CI we do extra sanity checks.
 test-%: AENEAS_OPTIONS += -checks
-else
-test-%: check-charon
 endif
 
 # Translate the given rust file to available backends. The test runner decides
 # which backends to use and sets test-specific options.
+# Note: the tests have the fulle file name: `test-arrays.rs`, `test-loops.rs`, `test-betree`.
 .PHONY: test-%
-test-%:
+test-%: build-dev
 	$(TEST_RUNNER_EXE) $(CHARON_EXE) $(AENEAS_EXE) $(LLBC_DIR) $(INPUTS_DIR)/"$*" $(AENEAS_OPTIONS)
 	echo "# Test $* done"
 
-- 
cgit v1.2.3