diff --git a/share/Makefile.headers b/share/Makefile.headers index 12f55b36c3bbe6703a86587882c26220424f1ed2..7783e0955e2a1acbe1660f842cf723b9766b4931 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)