Skip to content

Label relevant GitHub issues and pull requests with the "VIP" label #881

New issue
New issue
Open
Open
Label relevant GitHub issues and pull requests with the "VIP" label#881
Labels
VIPPull requests done by participants of the VIP programme.difficulty: 0A label for feature requests that should be easyhelp wantedA label for issues or PRs where help is wantedminorA label for PRs or issues that are minor in some sense.newcomer-friendlyA label for issues that someone thought might be friendly newcomers.technicalA necessary technical change, not interesting mathematically/feature-wise
@wilfwilson

Description

@wilfwilson
wilfwilson
opened on Nov 12, 2025

I added a label called "VIP" that I think will be handy for making it easy to find those contributions made by VIPers.

Perhaps one of those keen VIPers would like to look through old open/closed PRs (especially PRs, but also issues if they're mega keen), and label any pull requests made by students during their VIP times. 🙂

Metadata

Metadata

Assignees

No one assigned

    Labels

    VIPPull requests done by participants of the VIP programme.difficulty: 0A label for feature requests that should be easyhelp wantedA label for issues or PRs where help is wantedminorA label for PRs or issues that are minor in some sense.newcomer-friendlyA label for issues that someone thought might be friendly newcomers.technicalA necessary technical change, not interesting mathematically/feature-wise

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions