On , I learnt ...
About Github’s involves:$username
search filter
There’s a plethora of filters that can be used with Github’s search functionality.
An interesting filter is involves:$username
which selects
issues or pull requests where the user:
- Is the author
- Has commented
- Has been mentioned
- Has been assigned
- Has been requested as a reviewer
This can be useful to get an overview of a team’s activity over some period. You
can use the updated:>YYYY-DD-MM
filter to restrict the results to pull
requests with recent activity.
I discovered this when trying to find how to select pull requests authored by a
set of users. This isn’t possible in the pull request search (URL path
/pulls
); only the last author is used. But it is possible in the more general
search (URL path /search
) which has a different display format.
This Stack Overflow post contained the pertinent advice.