Build #255 (Jan 21, 2020 12:39:50 AM)

PR #2665: Changes to fix #2648

	No changes.
	GitHub pull request #2665 of commit a0422bdfe6b4a51d54f9f64d80989015ca6fde99, no merge conflicts.
	Aborted by user yonghong-song

Configurations