New label: Propose Merge without Discussion

FYI:

After several weeks of constructing the “review of open pull requests
and issues” part of the agenda by hand, I’m spending a few minutes
pulling together some XSLT to build that automatically (or mostly
automatically, anyway). To that end, I’ve added a new label to identify
PRs that should be in the “merge without discussion category.”

Removing the label won’t change the agenda after it’s published, of
course, but just let me know if you think something is mislabeled.

                                        Be seeing you,
                                          norm

--
Norm Tovey-Walsh
Saxonica

Received on Monday, 23 October 2023 08:26:55 UTC