From 9f832e74c055a40b2465aed83c99104eb165f511 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?C=C3=A9cile=20RUET-CROS?= <cecile.ruet-cros@cea.fr> Date: Thu, 22 Aug 2024 09:57:46 +0200 Subject: [PATCH] [w] remove wp_region from test config --- src/plugins/wp/tests/ptests_config | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/plugins/wp/tests/ptests_config b/src/plugins/wp/tests/ptests_config index 5221e8c0f16..d71d6024da0 100644 --- a/src/plugins/wp/tests/ptests_config +++ b/src/plugins/wp/tests/ptests_config @@ -1,8 +1,8 @@ DEFAULT_SUITES= wp wp_acsl wp_plugin wp_ce wp_bts wp_store wp_hoare -DEFAULT_SUITES= wp_typed wp_usage wp_gallery wp_manual wp_region wp_tip +DEFAULT_SUITES= wp_typed wp_usage wp_gallery wp_manual wp_tip qualif_SUITES= wp wp_acsl wp_plugin wp_bts wp_store wp_hoare -qualif_SUITES= wp_typed wp_usage wp_gallery wp_manual wp_region wp_tip +qualif_SUITES= wp_typed wp_usage wp_gallery wp_manual wp_tip qualif_SUITES= why3 ce_SUITES= wp_ce -- GitLab