Build #888 (16/10/2019, 3:09:07 PM)

	Changes General: updated our different developer Shell scripts. (details / githubweb)
	Started by upstream project OpenCOR_Linux build number 888 originally caused by: GitHub pull request #2192 of commit 6f60993bdde226d7e8fa8a448f8e68a6c6a70c87, no merge conflicts.
	This run spent: 1 ms waiting; 10 min build duration; 10 min total from scheduled to completion.
	Revision: e766a87abec1c1e9e21c1bc62eeebf8796bec3f5 Repository: https://github.com/opencor/opencor.git refs/remotes/origin/pr/2192/merge