From 29f52e095f20a38f753e2c14d89a6a9219a6e8b6 Mon Sep 17 00:00:00 2001 From: Allan Blanchard <allan.blanchard@cea.fr> Date: Mon, 25 Jul 2022 16:15:51 +0200 Subject: [PATCH] [headers] strict headers by default --- share/Makefile.headers | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/share/Makefile.headers b/share/Makefile.headers index 12f55b36c3b..7783e0955e2 100644 --- a/share/Makefile.headers +++ b/share/Makefile.headers @@ -30,9 +30,9 @@ # Must be unset (for external plugins) and set (for FRAMA-C kernel) FRAMAC_HDRCK?= -# Can be set to yes +# Can be set to no # - yes: adds "-exit-on-warning" option to "frama-c-hdrck" -HEADER_STRICT?= +HEADER_STRICT?=yes # Defines where to find the header directories HEADER_DIRS?=headers $(wildcard src/plugins/*/headers) -- GitLab