[soci-users] Changing the default branch in the Github repository?

[Vadim Z. <vz...@ze...>]

 Hello,

 Could one of the owners of the Github repository (Mateusz or Pawel if I'm
not mistaken) please change the default branch to "develop"? It's not very
convenient to have to select it explicitly for each new PR as "master" is
the default right now and, of course, it also risks encouraging people
submitting (and misguided developers such as me applying...) the PRs to the
master branch which is not supposed to be touched directly with the git
flow that we're supposed to use.

 TIA!
VZ