Skip to content

Conversation

yoshihiro503
Copy link
Contributor

Motivation for this change

fixes #1702

The make html comman generates rocqnavi HTML, but we have now created an HB graph to display in the index.

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

@yoshihiro503 yoshihiro503 force-pushed the yoshihiro503@rocqnavi-hb-graph branch from d515937 to 3860fb1 Compare September 17, 2025 05:08
@yoshihiro503 yoshihiro503 force-pushed the yoshihiro503@rocqnavi-hb-graph branch from 747cb31 to 2e8d397 Compare September 17, 2025 07:35
@affeldt-aist affeldt-aist added the documentation 📝 This issue/PR is about documentation of the library / repository label Sep 18, 2025
@affeldt-aist affeldt-aist added this to the 1.14.0 milestone Sep 18, 2025
@affeldt-aist affeldt-aist self-requested a review September 18, 2025 14:49
@affeldt-aist affeldt-aist merged commit 1c65191 into math-comp:master Sep 18, 2025
67 checks passed
hoheinzollern pushed a commit to hoheinzollern/analysis that referenced this pull request Sep 22, 2025
* CI: 📝 👷 `make html` generate hierarchy graph

* Rocqdoc HTML: 💄 👷 🔧 🔨 Introduce blacklist and type infomation tooltips

* CI: fix CI to use rocqnavi release 0.3.1
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

documentation 📝 This issue/PR is about documentation of the library / repository

Projects

None yet

Development

Successfully merging this pull request may close these issues.

More robust command in Makefile.common to generate the documentation

2 participants