Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Need an "ignore" option? #246

Open
wseltzer opened this issue May 19, 2022 · 1 comment
Open

Need an "ignore" option? #246

wseltzer opened this issue May 19, 2022 · 1 comment

Comments

@wseltzer
Copy link
Member

Where a participant leaves the WG after making a PR but before the PR is merged, the bot flags it. The participant had made the commitment, so it would be good to have a way to dismiss the flag without asserting "non-substantive".

See e.g. w3c/webauthn#1663

@dontcallmedom
Copy link
Member

The few times I've hit this situation, I handle it by adding a comment in the PR that explains the situation and merge without further ado.

(but to be clear, I'm not not pushing back against adding an escape hatch to the tool either)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants