Skip to content

CI: Use extr-dev opam repository while generating the Rocqnavi doc#2005

Merged
affeldt-aist merged 1 commit into
math-comp:masterfrom
proof-ninja:yoshihiro503@ci-use-extr-dev
Jun 27, 2026
Merged

CI: Use extr-dev opam repository while generating the Rocqnavi doc#2005
affeldt-aist merged 1 commit into
math-comp:masterfrom
proof-ninja:yoshihiro503@ci-use-extr-dev

Conversation

@yoshihiro503

@yoshihiro503 yoshihiro503 commented Jun 24, 2026

Copy link
Copy Markdown
Contributor
Motivation for this change

fixes #2006

Checklist
  • added corresponding entries in 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 preferentially merged into master.
  • PRs with disorganized commits are very likely to be squash-rebased.
Reminder to reviewers

@affeldt-aist affeldt-aist added documentation 📝 This issue/PR is about documentation of the library / repository build/continuous integration ⚙️ This issue/PR is about the build process or CI labels Jun 27, 2026

@affeldt-aist affeldt-aist left a comment

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thank you!

@affeldt-aist affeldt-aist merged commit 4eaa6fb into math-comp:master Jun 27, 2026
45 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

build/continuous integration ⚙️ This issue/PR is about the build process or CI documentation 📝 This issue/PR is about documentation of the library / repository

Projects

None yet

Development

Successfully merging this pull request may close these issues.

CI failures when MathComp dev version is picked up

2 participants