Skip to content

Commit 2e5e368

Browse files
authored
Rocqnavi: 👷📝 Resolve The Broken link to mathcomp-order (#1917)
* chore: 👷📝 Resolve The Broken link to mathcomp-order in Rocqnavi documents
1 parent febbfcf commit 2e5e368

File tree

1 file changed

+1
-0
lines changed

1 file changed

+1
-0
lines changed

Makefile.common

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -118,5 +118,6 @@ html: build $(DOCDIR)/dependency_graph.dot
118118
-structure-graph $(DOCDIR)/hierarchy_graph.dot \
119119
-index-blacklist etc/rocqnavi_index-blacklist \
120120
-show-type-information-using-coqtop-process \
121+
-external https://math-comp.github.io/htmldoc_2_5_0/ mathcomp.order \
121122
-external https://math-comp.github.io/htmldoc_2_5_0/ mathcomp.ssreflect \
122123
-external https://math-comp.github.io/htmldoc_2_5_0/ mathcomp.algebra

0 commit comments

Comments
 (0)