Docs/manual.de.texi:
  Fixed up German manual for mysql.de website (with English @node lines).
  @menu blocks are not filled so .info won't look nice.