issue !4#32257: Flexible linter false positives/negatives

Stream: triage

[Random Issue Bot]

Today I chose issue #32257 for discussion!

Flexible linter false positives/negatives
Created by @None (@SnirBroshi) on 2025-11-29
Labels:

Is this issue still relevant? Any recent updates? Anyone making progress?

[Snir Broshi]

I still don't understand why the bot fails to tag me

[Bryan Gin-ge Chen]

The code for the tagging is here: https://github.com/leanprover-community/azure-scripts/blob/5e7e0c784357724b6da37da613bc28c6211cc200/post_issue_on_zulip.py#L75

Looks like it just uses the name and login field from GitHub and the name field on your GitHub profile is blank: https://github.com/SnirBroshi

We could probably make it more sophisticated, but it hasn't been requested up to this point.

[Snir Broshi]

Bryan Gin-ge Chen said:

Looks like it just uses the name and login field from GitHub and the name field on your GitHub profile is blank: https://github.com/SnirBroshi

Thanks! I'll update it.
Can we make it use the Zulip to GH user translation that exists in this Zulip? Is that mapping already aggregated somewhere, then we can reverse the mapping?