I volunteer for being a maintainer (for all parts of all databases --- I'm not sure differentiating by parts is useful at this stage: a maintainer should abstain from approving something he does not understand, and I certainly will). I think I have no GitHub permissions, so you may open them when you have time. Thanks. Benoît
On Wednesday, December 15, 2021 at 11:19:07 AM UTC+1 Alexander van der Vekens wrote: > In general, providing and handling PRs should be as simple as possible. I > am not very experienced with Git, and I was happy that everything which was > essential needed worked: As long as there were no merge conflicts, I just > pushed my changes to my forked repository using GitHib Desktop, and a PR > was created automatically by Github. If there were merge conflicts, I > updated my forked repository by pulling the latest version of set.mm.git > develop, resolving the merge conflicts, and pushed again. There should be > not (much) more I have to do. > > About the reviews and maintainers: we must distinguish between reviewers > and persons performing the merging: Since it seems that I have only > restricted permissions (no write permissions?), I can only be a reviewer > and could approve PRs. Two approvals should be sufficient for changes of > the main part (except moving theorems from mathboxes only, see below), and > no approval for changes in the own mathbox (the person performing the > merging should have a quick look at it). Changing other mathboxes are > sometimes required (e.g. if theorems are moved to the main part, or > maintenace actions are performed, e.g. proof minimizations) - for this, > maybe only one approval (not necessarily by the mathbox owner(s)) should be > sufficient. > > I could volunteer for being a maintainer for set.mm, Parts > 2,5,6,7,8,10,11,14,16. > > > On Tuesday, December 14, 2021 at 10:43:13 PM UTC+1 vvs wrote: > >> Personally, I like seeing all the commits in my git log history. Using >>> bisect I can generally piece together what happened when. I often use the >>> PR history, but I'd hate to not have a local copy of the history to refer >>> to. >>> >> >> I'd say that it would be made simpler by a more simple history. And vice >> versa: if there are lots of intertwined commits bisecting will be more >> difficult. >> >> But it shows that it's more important to have simple PRs in a first place >> rather then relying on squashing it afterwards. >> > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/64cb1a13-ad03-4552-a80c-d9ceb7e6e1c2n%40googlegroups.com.
