[makefile] fixes testing aliases when plugins are disable

Makefile

@@ -152,6 +152,9 @@ FRAMAC_WTESTS:=$(FRAMAC_PTESTS_SRC)/wtests.exe
 # Frama-C also have ptest directories in plugins, so we do not use default
 PTEST_ALL_DIRS:=tests $(wildcard src/plugins/*/tests)
 
+# Test aliasing definition allowing ./configure --disable-<plugin> 
+PTEST_ALIASES:=@tests/ptests @src/plugins/ptests
+
 # Ptests needs config.sed so that dune can build Frama-C (if it is not built)
 PTEST_DEPS:=config.sed
 

share/Makefile.testing

@@ -38,6 +38,8 @@ PTEST_DIRS?=$(PTEST_ALL_DIRS)
 PTEST_DEPS?=
 # Indicate whether we use global WP cache
 PTEST_USE_WP_CACHE?=no
+# Defines the related dune targets
+PTEST_ALIASES?=$(addsuffix /ptests,$(addprefix @,$(PTEST_DIRS)))
 
 ifneq ($(FRAMAC_WP_QUALIF),)
 FRAMAC_WP_CACHEDIR=$(FRAMAC_WP_QUALIF)
@@ -59,9 +61,6 @@ endif
 
 ##########################################################################
 
-# Defines the related dune targets
-PTEST_ALIASES=$(addsuffix /ptests,$(addprefix @,$(PTEST_DIRS)))
-
 .PHONY: tests.info
 tests.info:
 	echo "FRAMAC_WTESTS='$(FRAMAC_WTESTS)'"