Merge branch 'next' into tmp

Conflicts:
	run_jenkins_compilation.sh