Open JasonGross opened 2 years ago
There's a hidden target </code> and a misleading target ci-unimath</summary> at https://github.com/coq/coq/pull/14748#issuecomment-1003116849
</code>
ci-unimath</summary>
Alternatively, we should just stop looking for targets after the first ` or < or >
`
<
>
There's a hidden target
</code>
and a misleading targetci-unimath</summary>
at https://github.com/coq/coq/pull/14748#issuecomment-1003116849