> I am less concerned about losing this kind of meta-info, as I expect we would continue discussion primarily on the mailing list.
Would you/we?
The initial suggestion mentioned pull-requests as being easier to handle than discussing patches over mailing lists - to which personally I agree (though I don't claim everyone should agree to that).
PRs carry discussions - which typically happen on the PR "page", on github and the github hosting would also be quite more useful if people can report bugs via github.
Otherwise, if there's no intention to use the github facilities which make collaboration easier and more visible, what's the point of moving to github? Just a different git-repo host?
On Sunday, October 16, 2016 4:25 PM, David Mertens <address@hidden> wrote:
I am less concerned about losing this kind of meta-info, as I expect we would continue discussion primarily on the mailing list. Mailing lists seem to me to be much better venues for discussion than the facilities provided by github.
My bigger concern is: who would be the project managers? Who would manage pull requests? I would volunteer for some of it, but I could only guarantee responsiveness during winter and summer breaks, and would want to hand off responsibility during my school's semesters. Are others willing to step up? If not, we shouldn't move to a github/pull-requests workflow.
David