> Date: Thu, 21 Jan 2021 18:18:36 +0000 > From: Andrew Burgess <andrew.burgess@embecosm.com> > Cc: Eli Zaretskii <eliz@gnu.org> > > Thanks for the feedback. > > The patch I pushed is below, I believe this addresses all of your > feedback. Yes. One nit is that @menu is better placed at the end of a node, not at its beginning.