Document that undefined %prec identifier warnings will remain.

[bison.git] / THANKS

diff --git a/THANKS b/THANKS
index a417bbc0e981e142f20f3c4e1d9d53a46c66d6df..75a09bcedbe7e0b38f75eb5cd97c820e84cc2cde 100644 (file)
--- a/THANKS
+++ b/THANKS
@@ -24,6 +24,7 @@ Christian Burger          cburger@sunysb.edu
 Cris Bailiff              c.bailiff+bison@awayweb.com
 Cris van Pelt             cris@amf03054.office.wxs.nl
 Csaba Raduly              csaba_22@yahoo.co.uk
+Dagobert Michelsen        dam@baltic-online.de
 Daniel Hagerty            hag@gnu.org
 David J. MacKenzie        djm@gnu.org
 Derek M. Jones            derek@knosof.co.uk