Thanks! It looks like all of the outstanding comments have been addressed. I don't see any obvious problems. I'm not very familiar with the functioning of the .github repository. It seems that we can't really preview its effect on how other repositories in the org look, so we might have to merge it to see?
People can now submit pull requests for the files listed above.
Just checking: the github.com copy is authoritative and there is no git.torproject.org repository?
People can now submit pull requests for the files listed above.
Just checking: the github.com copy is authoritative and there is no git.torproject.org repository?
.github is a GitHub-specific configuration repository.
So I didn't set up a canonical repository on git.torproject.org, and I don't think we need one.
People can now submit pull requests for the files listed above.
Just checking: the github.com copy is authoritative and there is no git.torproject.org repository?
.github is a GitHub-specific configuration repository.
So I didn't set up a canonical repository on git.torproject.org, and I don't think we need one.
Thanks!
Given that this change affects more than the network team, maybe we should ask other teams for objections before merging?
Good catch! The license file isn't part of this PR, though; it looks like github provided it with the initial repository.
Given the history of this ticket, I think our best bet is for me to raise this for more general discussion again and propose a way forward. Namely, I think we should merge the PR, and then fix up whatever remaining issues we find.
I'll bring this up at the all-hands on wednesday and propose that we go ahead that way.
Some issues I would fix post-merge are:
Stop recommending trac as a support forum.
Explicitly list which repositories are "owned"/maintained by which teams, with a table or list covering every repo we have.
Sent an email to tor-internal@, giving a last chance to object before we merge, and asking whether we shouldn't just give ownership of this component to the web team.