Build #47 (Aug 6, 2019 3:20:39 PM)

PR #2484: man: fixes some man pages

	No changes.
	GitHub pull request #2484 of commit 33c9c571057b75ec979cc74121a0d3cb3a19be1b, no merge conflicts.

Configurations