bot
bot copied to clipboard
CI targets should be sanitized or quoted
There's a hidden target </code> and a misleading target ci-unimath</summary> at https://github.com/coq/coq/pull/14748#issuecomment-1003116849
Alternatively, we should just stop looking for targets after the first ` or < or >