On 4 Apr 2012, at 12:33, Akim Demaille wrote: >> I took it down from GIT, and the index still has the following: >> YYABORT; >> YYACCEPT; >> yyclearin; >> yyerrok; >> YYERROR; > > It is installed in maint, it will show in master when I merge.
OK. It looks fine. Hans
