I feel like it would be almost the same, and easier, to just build the docs every time?

I feel like it would be almost the same, and easier, to just build the docs every time?

Sure, that is what I was considering initially, but perhaps it's not necessary to rebuild docs when adding type hints to tests (e.g. #7816) or updating dependencies (e.g. #7752).

I don't have a strong preference either way, this just seems simpler to me.

Looks good!

@nulano Thanks again for all your help triaging issues and reviewing PRs! Can we add you as a triager to this repo? It means you can label PRs yourself, and also close/re-open issues/PRs (for example, closing as duplicate). You could also join our Discord/Slack. What do you think? :)

Can we add you as a triager to this repo? It means you can label PRs yourself, and also close/re-open issues/PRs (for example, closing as duplicate).

Sure, we could give that a go. :)

You could also join our Discord/Slack. What do you think? :)

Feel free to send me an invite; I should have the same username on Discord, but don't actively use it.

Great, Discord/Slack invites sent!

Hmm, I don't see anything. Did Discord/Slack ask for an email address to send the invite? My email server's boot drive just died yesterday so I won't be able to receive email for a few days on the email address I use on GitHub (GitHub invite should be fine - I've temporarily changed my GitHub notification address to use my private email). I'll let you know when I've got it fixed.

And accepted!

It means you can label PRs yourself, and also close/re-open issues/PRs (for example, closing as duplicate).

But I don't see any changes in the GitHub interface, e.g. I still can't see an edit labels button on this PR like I can in projects in other organizations.

I sent invite links from my email to the email address on your GitHub profile. I've also sent a friend request on Discord, I don't think it's possible to invite someone directly who's "unknown".

@aclark4life Did you also give triage role/permission to the team?

@aclark4life Did you also give triage role/permission to the team?

No, I clicked around a bit and couldn't find out where/how to do that, at which point I got generally confused about GitHub's roles/teams/people/permissions/sigh. Then I remembered in the early days they made some major change to that system and I don't think I've understood what's going on since then 🤔

Annoyingly, nothing happens when I go here except I can filter stuff.

Sooo… we need to find where/how to give triage/role permission and the only explanation for the missing configuration option I can think of is … we need enterprise? 🤷

Done!

I sent invite links from my email to the email address on your GitHub profile. I've also sent a friend request on Discord, I don't think it's possible to invite someone directly who's "unknown".

I didn't see the friend request when I checked earlier, but I just found and accepted it.

My email server's boot drive just died yesterday so I won't be able to receive email for a few days on the email address I use on GitHub. [...] I'll let you know when I've got it fixed.

I could get the email server running again with my new boot drive, but unfortunately I didn't have a backup of the email server config (among others) and I'm still waiting for a quote on data recovery (I was supposed to receive it by now) to find out whether I have to redo it. :/

My email eventually bounced because it couldn't reach the server, but I've sent fresh invites via Discord 👍