I'm canceling CI here, since there are no code changes. I hope that's OK.
That's definitely the right thing to do. Sorry I didn't think to do that myself. Can that be done by adding [skip ci] to the PR title and text?
I think so, but I usually forget to do that, myself. I'm happy to cancel CI for you anytime if you forget. Much better than waiting on it!
I also don't have auth to merge this so I'll have to rely on one of the other contributors there.