[O] ox-texinfo: empty line before "* Menu:" is missing

[Jonas Bernoulli]

Hello

Given this Org file

  #+TITLE: Demo Manual
  #+TEXINFO_DIR_CATEGORY: Emacs
  #+TEXINFO_DIR_TITLE: Demo: (demo).
  #+TEXINFO_DIR_DESC: Demo.
  
  * Missing empty line
  
  There is text between the heading and the menu
  
  ** There is text before this menu
  ** the empty line before Menu IS missing
  
  * Has empty line
  
  ** There is no text between heading and this menu
  ** the empty line before Menu is NOT missing

using C-c C-e i i produces a texi file containing

  There is text between the heading and the menu
  @menu

and an info file containing

  There is text between the heading and the menu
  * Menu:

and that is then also displayed like that in Info.  But there should be
an empty line before "* Menu:".

This can be fixed in `org-texinfo-make-menu' by replacing
"@address@hidden menu" with "address@hidden@end menu".  In rare cases (which
I have not further investigated) this change leads to two empty lines in
the texi file where there should only be one, but these two empty lines
won't make it into the info file, which after all is what really matters
here, after all that's what the end-user will be looking at.

The behavior is currently the same in "maint" and "master".

  Best regards,
  Jonas