Marvin Reply wrote:
> There was a longish thread on debian-devel a while back (I can't find it
> right now) about using github for development. One of the points raised
> was that if you accept github pull requests (from their web UI), then
> those developers who do not have (and perhaps do not wish to get) github
> accounts cannot participate. If you disallow github pull requests and
> only accept git PRs (perhaps with a dedicated mailing list), than anyone
> can participate.
>
> I have never used the github UI, so I don't know how true this is, and I
> may have misunderstood what the problems were, but it is at least
> something to consider.
The idea is that all events on GitHub are forwarded to the vimdev
maillist. Christian had setup something for that. I believe this also
applies to pull requests.
I indeed prefer to discuss changes on the maillist, since everybody can
join and it keeps everything in one place. I also plan to keep
including patches as before, not directly using the pull request.
We'll see how it goes.
--
VOICE OVER: As the horrendous Black Beast lunged forward, escape for Arthur
and his knights seemed hopeless, when, suddenly ... the animator
suffered a fatal heart attack.
ANIMATOR: Aaaaagh!
VOICE OVER: The cartoon peril was no more ... The Quest for Holy Grail could
continue.
"Monty Python and the Holy Grail" PYTHON (MONTY) PICTURES LTD
/// Bram Moolenaar -- [email protected] -- http://www.Moolenaar.net \\\
/// sponsor Vim, vote for features -- http://www.Vim.org/sponsor/ \\\
\\\ an exciting new programming language -- http://www.Zimbu.org ///
\\\ help me help AIDS victims -- http://ICCF-Holland.org ///
--
--
You received this message from the "vim_dev" maillist.
Do not top-post! Type your reply below the text you are replying to.
For more information, visit http://www.vim.org/maillist.php
---
You received this message because you are subscribed to the Google Groups
"vim_dev" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
For more options, visit https://groups.google.com/d/optout.
