[PATCH] Fix html build with makeinfo 5.2

[Thomas Preudhomme]

HTML build fails with makeinfo 5.2 with the following error:

libgloss/doc/porting.texi:73: @menu seen before first @node
libgloss/doc/porting.texi:73: perhaps your @top node should be wrapped in 
@ifnottex rather than @ifinfo?

Following the advice indeed solve the issue while still allowing pdf, dvi and 
info builds to work.


diff --git a/libgloss/doc/porting.texi b/libgloss/doc/porting.texi
index 
9e1d9286e8c858e9a4982ea4efc0ceab206a119c..9beda39e5a0434817b4b3fb224d2c74831740a58 
100644
--- a/libgloss/doc/porting.texi
+++ b/libgloss/doc/porting.texi
@@ -39,7 +39,7 @@ Permission is granted to copy and distribute translations of 
this manual
  into another language, under the above conditions for modified versions.
  @end titlepage

-@ifinfo
+@ifnottex
  @format
  START-INFO-DIR-ENTRY
  * Embed with GNU: (porting-).         Embed with GNU
@@ -62,7 +62,7 @@ into another language, under the above conditions for modified 
versions.
  @node Top
  @top Embed with GNU

-@end ifinfo
+@end ifnottex
  @strong{Rough Draft}

  The goal of this document is to gather all the information needed to


Is this ok for master branch?

Best regards,

Thomas