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.