Filtering users by their GitHub user ID

Filtering users by their GitHub user ID: a task in MiMo-V2.6-RL-harbor-code: MiMo-V2.6-RL Code (Harbor) (Harbor dataset). We have a Coder deployment where most users sign in via GitHub OAuth. The users table already stores each user's GitHub user ID (it gets populated when they log in), but there…