From af076fe42278e155a45ae6a23f69dc72491a7412 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Mon, 27 Nov 2023 09:08:06 +0100
Subject: [PATCH] [doc] prefer 'make default-tests' for external users

---
 CONTRIBUTING.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index 6e379ee8433..e5b6df0ec5b 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -78,7 +78,7 @@ The detailed steps to submit a contribution to Frama-C are:
   needed), and `make headers` to fix them.
 
 8. Locally run the test framework of Frama-C by typing
-  `make tests`
+  `make default-tests`
   in your terminal (you should be in the Frama-C root directory).
 
 9. Locally add (if needed) and commit your contribution.
-- 
GitLab