[FYI] {yacc-work} merged maint into yacc-work

[Stefano Lattarini]

I've merged maint in yacc-work, fixed minor fallout (in the same merge
commit), and pushed.

Regards,
  Stefano