bot icon indicating copy to clipboard operation
bot copied to clipboard

Published 20 hours ago • verified publisher icon coq

CI targets should not match substrings ("the" should not match "category_theory")

Open JasonGross opened this issue 3 years ago • 2 comments

https://github.com/coq/coq/pull/14748#issuecomment-1003116849

JasonGross avatar Dec 30 '21 17:12 JasonGross

But not providing the ci- prefix is OK.

Zimmi48 avatar Dec 30 '21 20:12 Zimmi48

I think the reason I originally did this was to also not have to provide library: vs plugin:, but we should just strip these things off both the request and the string we're comparing with

JasonGross avatar Dec 30 '21 20:12 JasonGross