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) diff --git a/src/plugins/eva/.gitattributes b/src/plugins/eva/.gitattributes index e62b79b9279d0dae86ee89c3782e8600365bb619..deef66cd8639e14890c171d484edc68e3be4a093 100644 --- a/src/plugins/eva/.gitattributes +++ b/src/plugins/eva/.gitattributes @@ -2,5 +2,6 @@ # HEADER_SPEC: .ignore # ######################## +/Eva.header header_spec=.ignore /Changelog_non_free header_spec=.ignore /legacy/TOREMOVE header_spec=.ignore