A small risk I can see (I hope I'm wrong) is that we would end up with a pretty long list of pending PRs and the n_th PR in the queue could be merged with the repository when it was submitted, but it will often conflict with one of the PRs ahead in the queue.
Is this something to be worried about? Glauco Il giorno lunedì 13 dicembre 2021 alle 19:20:27 UTC+1 David A. Wheeler ha scritto: > Sadly, Norm is no longer with us. We're going to have to work out next > steps. > > Norm typically made the final decision of what to accept or not accept > into the set.mm database. > We're going to have to find another process. > > I would suggest, for now, that proposed changes continue to be added as > GitHub pull requests. > Obviously any change *must* pass the automated checks to be considered for > merging. > Others can "approve" by going to the "Files Changed" tab and click on > "review changes". > If you approve, click on "approve" and then "submit review". Or you could > just say "+1" as a comment. > If after several days (I suggest 5) there's another approver who has > *previously* had a change approved, > and no disagreement, I suggest merging it. If there's disagreement, > discuss in the comments to > try towards resolution (& if it's more contentious, also involve the > mailing list). > > We don't have to use this process. I'm just suggesting *a* process we can > use. > If anyone would prefer another process, please speak up. > > --- David A. Wheeler > > -- 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/ab1fbf3a-1f43-4608-ad9e-e970b5338d11n%40googlegroups.com.
