-
Notifications
You must be signed in to change notification settings - Fork 632
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.
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
Wrong section for Dune entry in Changelog #18407
Labels
kind: documentation
Additions or improvement to documentation.
Milestone
Comments
olaure01
added
the
kind: documentation
Additions or improvement to documentation.
label
Dec 14, 2023
That's master not 8.19 |
olaure01
changed the title
Wrong section for Dune entry in Changelog 8.19
Wrong section for Dune entry in Changelog
Dec 14, 2023
Oups sorry, thanks. |
SkySkimmer
added a commit
to SkySkimmer/coq
that referenced
this issue
Dec 14, 2023
I'm sorry, I think indeed I typed the wrong number. Thanks for the report! |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Description of the problem
The entry about Dune version should probably be in Infrastructure and dependencies rather than "Standard library".
The text was updated successfully, but these errors were encountered: