bot icon indicating copy to clipboard operation
bot copied to clipboard

CI targets should be sanitized or quoted

Open JasonGross opened this issue 4 years ago • 1 comments

There's a hidden target </code> and a misleading target ci-unimath</summary> at https://github.com/coq/coq/pull/14748#issuecomment-1003116849

JasonGross avatar Dec 30 '21 17:12 JasonGross

Alternatively, we should just stop looking for targets after the first ` or < or >

JasonGross avatar Dec 30 '21 17:12 JasonGross