Corelib links for rc1 #76
Conversation
mattam82
force-pushed
the
corelib-link
branch
from
186af3c to
e7c589d
Compare
|
That's a lot of links! |
| let pre, version = | ||
| match String.split_on_char '.' v with | ||
| | x :: y :: z :: _ -> false, x ^ "." ^ y ^ "." ^ z | ||
| | x :: y :: [] -> | ||
| (match String.split_on_char '+' y with | ||
| | [] -> assert false | ||
| | [y] -> false, x ^ "." ^ y | ||
| | y :: _ -> true, x ^ "." ^ y) | ||
| | _ -> invalid_arg (v ^ ": invalid version") | ||
| in | ||
| if pre then "v" ^ version | ||
| else "V" ^ version |
There was a problem hiding this comment.
Note that in theory, the tag version (starting with V) would work fine for the rc as well: https://rocq-prover.org/doc/V9.0+rc1/refman/index.html exists for instance.
The logic of calling the patch function could have been replaced by no call at all.
That being said, I am fine with considering that we link to a branch while in pre-release and to a tagged version afterward.
Note though that so far, we only updated links to the reference manual when releasing the final .0 version. The question then is whether we consider that this is an exceptional case (since the rocq-prover.org website is still in preview) or whether it will keep beeing that way (switching at the time of the rc for 9.1 as well).
Supersedes #71
Closes: #71