Hi, Actually, text after .toctree are included at the end of entire info page.
For now, not using text after .toctree is a reasonable work around. But the best solution is to write extension to emmit such text after .toctree immediately after @menu section in *.texi file. So let's make this bug report tracking this extension while implementing workaround for https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=934526 Osamu
