On Saturday, 14 May 2016 at 19:34:12 UTC, Walter Bright wrote:
On 5/14/2016 9:31 AM, Jonathan M Davis via Digitalmars-d wrote:
On Saturday, May 14, 2016 13:27:17 ZombineDev via
Digitalmars-d wrote:
Or just unsubscribe those groups from github. dmd, for
example,
doesn't get messages from github anymore.
I actually like having a mailing list that gets all of those
messages,
though it really doesn't work to have it then be used for
normal
communication.
I like getting the github messages for another reason. There's
an awful lot of value in those messages. If github goes dark
for whatever reason, we all have copies of the git
repositories, that's not a problem. But the messages would
disappear.
I.e. it's a (crude) backup of the github messages.
But we just store the pushed commits there (aka history) - this
is contained in every git repo and can be easily accessed by `git
log`.
So if having a backup of the Github PRs important to us, we
should have a proper solution that uses the Github API [1] and
stores the issues in a machine-friendly format from time to time.
[1] https://developer.github.com/v3/pulls/
Anyhow I think the idea was to split off the main thread
"General" in different categories like:
- DMD
- DRuntime
- Phobos
- Design/Study
- Other/off-topic
