-
Notifications
You must be signed in to change notification settings - Fork 2.4k
Add title for some dialogs and avoid hardcoding the text of the discard changes dialog #3846
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
Conversation
the CONTRIBUTORS script is really broken. Do I need to change it in EVERY PR I do? |
adding my name to contributors for the third time
apparently the only way to retrigger CI here is doing a push force, and the odd error still persists. Not sure if I can do anything now |
Each of the changes you've made to that file have been listed as your capitalized noreply username: dae@mb:Work/desktop/anki% git log --pretty=format:%ae -- CONTRIBUTORS | grep -i brayan The last check failed because your username for the latest commit was 69634269+brayandso@. How did you author and push the commits? What do you have your git author email configured as? |
Under my branch:
Looks alright to me |
That's lowercase, whereas your GitHub username is mixed case. Email addresses are theoretically case-sensitive: https://stackoverflow.com/questions/9807909/are-email-addresses-case-sensitive. I don't recall any other users hitting this so far, but happy to accept a PR that makes the check in minilints case-insensitive. |
For checking the GitHub account, only the ID should matter. The username shouldn't. |
This is a check of the git commit history, and commits can be made outside of GitHub / with non-GitHub accounts in some cases (when PRs are not squashed, commits are cherry-picked outside GitHub, etc). It's not a GitHub-specific check. |
Similar to #3838.
The commits should be self-explanatory