manual.texi	Add note about "source" to one batch file section,
manual.texi	make it more obvious to readers that there is another
manual.texi	batch file section with more information.


Docs/manual.texi:
  More pertinent @ref.