Jim is the release manager during my vacation.
Merge branch 'next' into tmp

Conflicts:
	run_jenkins_compilation.sh