Skip to content

Rocqnavi: 📝 Use Rocqnavi's development HEAD instead of the released version - #2131

Open
yoshihiro503 wants to merge 1 commit into
math-comp:masterfrom
proof-ninja:yoshihiro503@rocqnavi-dev-HEAD
Open

yoshihiro503 wants to merge 1 commit into
math-comp:masterfrom
proof-ninja:yoshihiro503@rocqnavi-dev-HEAD

Conversation

@yoshihiro503

Copy link
Copy Markdown
Contributor
Motivation for this change

Documentation generation (make html) now uses the latest development version of Rocqnavi, instead of the latest released version. This lets us use new Rocqnavi features/fixes before they're officially released.

Checklist
  • appended entries in the relevant sections of CHANGELOG_UNRELEASED.md
  • added corresponding documentation in the headers

Reference: How to document

Merge policy

As a rule of thumb:

  • PRs with several commits that make sense individually and that
    all compile are likely to be merged as they are into master.
  • PRs with disorganized commits are very likely to be squash-rebased.
Reminder to reviewers

This branch has not been deployed

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

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant