Element-Timing not found on ipr bot check

[npm1]

I see WICG/Element-Timing listed on https://labs.w3.org/repo-manager/repos but the ipr bot says it does not know about it on https://github.com/WICG/element-timing/pull/66. I don't imagine the repo name became case-sensitive match? Not sure why it's showing that error message, would appreciate some help. Thanks!

[deniak]

It actually is case-sensitive. That's something we should try to fix. In the meantime, I've renamed the repo in the repo-manager. Do you have admin rights on that repo to redeliver the webhook payload for that PR?

[npm1]

I do have admin rights, but not sure how to do that :S

[deniak]

Any chance you can grant me access to the repo settings temporarily?

[npm1]

Done

[deniak]

The bot should now pass. Feel free to remove my access to that repository.

[npm1]

Thank you :)