It is a fair question and to a fair extent I think we can rely on the
judgement of the person merging it about how long to wait (subject to
the more black and white rules about passing the automated checks and -
I suppose this is black and white except for mathboxes - having at least
one approval). That is, I think many of us have at least some feel for
whether there needs to be more discussion or there's a potential for
controversy.
We can also see whether merge conflicts of this sort end up being
frequent or rare. A bit hard for me to predict in advance, as it depends
on how often people change the same parts of (well, set.mm especially,
the other files to a smaller extent).
On 12/13/21 12:02 PM, Glauco wrote:
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 <http://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]
<mailto:[email protected]>.
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/ab1fbf3a-1f43-4608-ad9e-e970b5338d11n%40googlegroups.com
<https://groups.google.com/d/msgid/metamath/ab1fbf3a-1f43-4608-ad9e-e970b5338d11n%40googlegroups.com?utm_medium=email&utm_source=footer>.
--
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/a53643c7-278c-f406-ae60-110ce3f1bb65%40panix.com.
