Skip to content
Snippets Groups Projects
Commit f3df4c9f authored by Björn Brandenburg's avatar Björn Brandenburg
Browse files

work around Coq bug #18434

In Coq 8.18, coqdoc's --external flag had its arguments flipped (see
https://github.com/coq/coq/issues/18434). To work around this, we
provide both

	--external https://math-comp.github.io/htmldoc/ mathcomp

and

	--external mathcomp https://math-comp.github.io/htmldoc/

One will be understood by Coq 8.17 and earlier, the other works for
Coq 8.18.

This hack can be reverted when upgrading to a version of Coq in which
the regression has been fixed (presumably 8.19).
parent ebca70d9
No related branches found
No related tags found
1 merge request!337remove Makefile patching and fix links in spec
......@@ -59,7 +59,7 @@ mangle-namesCoqProject: commonCoqProject
-print | scripts/module-toc-order.py >> $(COQ_PROJ)
$(COQ_MAKEFILE): $(COQ_PROJ) scripts/Makefile.coq.patch
@coq_makefile -f $< -o $@ COQDOCEXTRAFLAGS = "--parse-comments --external https://math-comp.github.io/htmldoc/ mathcomp"
@coq_makefile -f $< -o $@ COQDOCEXTRAFLAGS = "--parse-comments --external https://math-comp.github.io/htmldoc/ mathcomp --external mathcomp https://math-comp.github.io/htmldoc/"
@# Patch HTML target to switch out color.
@# Also include Makefile.coqdocjs for 'htmlpretty' documentation target.
@patch -s < scripts/Makefile.coq.patch
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment