New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

"Doc: Show manual" command opens beta version #987

Closed

TheoWinterhalter opened this issue Jan 17, 2025 · 1 comment · Fixed by #1008

Labels

bug

Milestone

Next release (v2....

TheoWinterhalter commented Jan 17, 2025

Currently, using the "Doc: Show manual" command opens the beta version of the manual: https://coq.inria.fr/doc/master/refman/index.html

I'm guessing it should open the version corresponding to the Coq version that is currently being used, what do you think?

Collaborator

rtetley commented Jan 17, 2025

Ah yeah ! Definitely !

rtetley added the bug label

rtetley added this to the Next release (v2.2.4) milestone

rtetley mentioned this issue

feat: open doc at installed coq version #1008

Merged

rtetley closed this as completed in #1008

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment