Build #192 (Dec 24, 2019 12:26:03 AM)

PR #2665: Changes to fix #2648

	No changes.
	GitHub pull request #2665 of commit 09a821f9d24c607ddc662d859a545301a104404d, no merge conflicts.

Configurations