[boost] [GitHub] [PR] setting default branch to 'develop'

Hi, We sometimes forget to change the base branch of PR from 'master' to 'develop', even if we know PR should be made against 'develop' branch! To prevent from accidentally making PR against master branch, it'd be nice to **set the default branch to 'develop' branch** for Boost repositories on GitHub. (Then, the default base branch of PR would be set to 'develop' branch.) To change the default branch, it takes just a few clicks on web browser: https://help.github.com/articles/setting-the-default-branch/ Thoughts? Regards, Michel P.S. Some libraries have already done this, but most of Boost libraries don't do this yet.