*** empty log message ***

[splint.git] / src / bison.head

diff --git a/src/bison.head b/src/bison.head
index 9e8212d7c05f8697fc14e60cf197805f1110bd98..681fd145627cc8afb0e8f1d1d5aff630a3029565 100644 (file)
--- a/src/bison.head
+++ b/src/bison.head
@@ -52,5 +52,7 @@
 /*drl added 12/11/2002*/
 /*@-type@*/
 
+/*@-enummemuse@*/
+
 /* < end of bison.head > */