8000 Update parsing md & mention it in plugin tuto mlg files by SkySkimmer · Pull Request #20669 · rocq-prover/rocq · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Update parsing md & mention it in plugin tuto mlg files #20669

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
Open
wants to merge 2 commits into
base: master
Choose a base branch
from
Open

Update parsing md & mention it in plugin tuto mlg files #20669

wants to merge 2 commits into from

Conversation

SkySkimmer
Copy link
Contributor

VERNAC EXTEND doc should be reasonably complete with this.

We could also consider promoting parsing.md to a refman page.

SkySkimmer added 2 commits May 22, 2025 14:01
@SkySkimmer
Update parsing.md
08068bc 
VERNAC EXTEND doc should be reasonably complete with this.
@SkySkimmer
Mention parsing.md in plugin tuto mlg files
e8d8768
@SkySkimmer SkySkimmer requested review from a team as code owners May 22, 2025 12:03
@SkySkimmer SkySkimmer added the kind: documentation Additions or improvement to documentation. label May 22, 2025
@SkySkimmer SkySkimmer added this to the 9.1+rc1 milestone May 22, 2025
@coqbot-app coqbot-app bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label May 22, 2025
@SkySkimmer SkySkimmer removed the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label May 28, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
kind: documentation Additions or improvement to documentation.
Projects
None yet
Milestone
9.1+rc1
Development

Successfully merging this pull request may close these issues.
1 participant
@SkySkimmer
0