From 119e0065fdfd82d005ba631bf622b7a89de5c5e4 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Thu, 8 Sep 2022 10:35:59 +0200
Subject: [PATCH] [tests] add 'default-tests' target to only run default config
 tests

---
 share/Makefile.testing | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/share/Makefile.testing b/share/Makefile.testing
index 3569f03d45e..e7fae696d93 100644
--- a/share/Makefile.testing
+++ b/share/Makefile.testing
@@ -204,6 +204,11 @@ tests::
 endif # FRAMAC_WP_CACHEDIR
 endif # PTEST_USE_WP_CACHE
 
+.PHONY: default-tests
+default-tests: run-ptests
+	dune build --display short @ptests_config
+	$(MAKE) count-tests
+
 .PHONY: count-tests
 count-tests:
 	@echo "Number of *.{err,res}.log files:"
-- 
GitLab