I don't think it's to do with texinfo, the original texinfo source also has the extra spacing. (See the attached sample patch).
I'm also not sure why the source wraps at about the 72nd column. This makes the documentation artificially difficult to read on a large terminal. Surely the documentation viewer should perform the wrapping. (Either that or perhaps the info generation script can be configured to undo artificial line wrapping within a paragraph.)
--- bashref.texi 2005/09/11 00:09:38 1.1 +++ bashref.texi 2005/09/11 00:11:28 @@ -94,46 +94,27 @@ @menu * Introduction:: An introduction to the shell. - -* Definitions:: Some definitions used in the rest of this - manual. - +* Definitions:: Some definitions used in the rest of this manual. * Basic Shell Features:: The shell "building blocks". - * Shell Builtin Commands:: Commands that are a part of the shell. - * Shell Variables:: Variables used or set by Bash. - * Bash Features:: Features found only in Bash. - * Job Control:: A chapter describing what job control is and how Bash allows you to use it. - -* Using History Interactively:: Chapter dealing with history expansion - rules. - -* Command Line Editing:: Chapter describing the command line - editing features. - +* Using History Interactively:: Chapter dealing with history expansion rules. +* Command Line Editing:: Chapter describing the command line editing + features. * Installing Bash:: How to build and install Bash on your system. - * Reporting Bugs:: How to report bugs in Bash. - * Major Differences From The Bourne Shell:: A terse list of the differences between Bash and historical versions of /bin/sh. - * Copying This Manual:: Copying this manual. - * Builtin Index:: Index of Bash builtin commands. - * Reserved Word Index:: Index of Bash reserved words. - * Variable Index:: Quick reference helps you find the variable you want. - * Function Index:: Index of bindable Readline functions. - * Concept Index:: General index for concepts described in this manual. @end menu @@ -143,7 +124,6 @@ @chapter Introduction @menu * What is Bash?:: A short description of Bash. - * What is a shell?:: A brief introduction to shells. @end menu @@ -371,9 +351,7 @@ @section Shell Syntax @menu * Shell Operation:: The basic operation of the shell. - * Quoting:: How to remove the special meaning from characters. - * Comments:: How to specify comments. @end menu
