[boost] [github] default PR destination

Subject: [boost] [github] default PR destination
From: Tim Blechmann (tim_at_[hidden])
Date: 2014-01-04 06:51:00

hi all,

any opinion to change the default branch from "master" to "develop"?

with the boost branching model all contributions via github's pull
requests apparently have to go to "develop" rather than going directly
into "master", so this should be the default destination for pull
requests. github allows to set the default branch [1] ... not sure if
this has any other side effects, but i'd vote for changing the default
to "develop".

thoughts?
tim
[1] https://help.github.com/articles/setting-the-default-branch