Re: grub build failure - never mind :-(

[A. P. Garcia]

I'm sorry.  I got impatient and x-posted this from bug-grub@gnu.org just
before I received a fix.