Re: master branch in place of devel-3

[Justin Mclean]

Hi,

You can make the default branch something other than master in github by 
raising an infra JIRA, but it’s less work (and causes less confusion to users) 
to just work in master.

Thanks,
Justin