diff --git a/create_makefile.sh b/create_makefile.sh index 25f27433e4f9f189d09e77cab48150eef6ee1ca8..aeb68de0c2b09cadd7b29c0fe6094999e26dbd13 100755 --- a/create_makefile.sh +++ b/create_makefile.sh @@ -6,3 +6,7 @@ coq_makefile -f _CoqProject $(find -name "*.v" ! -name "*#*" ! -name "*eqdec*.v" # and cause clashes for files with the same name. This forces full filenames and # adds the rt. prefix sed -i 's|$(notdir $(^:.vo=))|$(addprefix rt., $(subst /,., $(^:.vo=)))|g' Makefile + +# Fix 'make html' so that it parses comments and has links to ssreflect. +sed -i 's|-interpolate -utf8|-interpolate -utf8 --parse-comments --external https://math-comp.github.io/math-comp/htmldoc/ mathcomp|g' Makefile +