On Tuesday, October 17, 2023 at 12:50:27 AM UTC+9 tobia...@gmx.de wrote:
I've now set some of the github checks as "required", so they get a small tag in the checks list. That should take care of (2). I am not sure if that helps or makes things worse, as that is one more thing to look and think. Having some checks with "Required" and some without makes things look more complicated. What should we think of a check not passed and not "Required". Should we ignore it? We should aim at "requiring" all checks passed (or skipped). Personally I am using the chrome extension mentioned above. That solves problems (1) and (3), and (2) is less a problem for me. The problems (1), (2), (3) seem basically problems that GitHub should solve by redesigning the checks list. I hope that they adopt the design of the chrome extension. -- You received this message because you are subscribed to the Google Groups "sage-devel" group. To unsubscribe from this group and stop receiving emails from it, send an email to sage-devel+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/sage-devel/921a1f15-3b68-4fb8-8909-5762d04af91an%40googlegroups.com.
