On Monday, January 3, 2022 at 7:21:20 AM UTC+1 [email protected] wrote: > I think we're all agreed that a bot would be better (although I now see > there would be more than one way to write it). I'm not trying to discourage > anyone from making a bot happen at all. > I agree with Jim and Mario. I view the current CI check as a temporary solution before the solution described by Mario is implemented. The discussion can be continued at https://github.com/metamath/set.mm/issues/2381
Benoît -- 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/99a5752e-e609-44af-9704-d83643680bd5n%40googlegroups.com.
