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

cleanup create_makefile.sh

1) rely on patch to actually patch the Makefile
2) move ineffective 'sed' hackery related to 'make validate'

Re 2), the sed script didn't actually modify the Makefile anyway
(unlear how long it has been ineffective), so let's just remove it.
parent 3b18aa36
No related branches found
No related tags found
No related merge requests found
...@@ -25,18 +25,7 @@ FIND_OPTS+=( -print ) ...@@ -25,18 +25,7 @@ FIND_OPTS+=( -print )
# Compile all relevant *.v files # Compile all relevant *.v files
coq_makefile -f _CoqProject $(find "${FIND_OPTS[@]}" ) -o Makefile coq_makefile -f _CoqProject $(find "${FIND_OPTS[@]}" ) -o Makefile
# Fix the 'make validate' command. It doesn't handle the library prefix properly
# and cause clashes for files with the same name. This forces full filenames and
# adds the rt. prefix
if [ "$(uname)" == "Darwin" ]; then
sed -i '' 's|$(notdir $(^:.vo=))|$(addprefix rt., $(subst /,., $(^:.vo=)))|g' Makefile
else
sed -i 's|$(notdir $(^:.vo=))|$(addprefix rt., $(subst /,., $(^:.vo=)))|g' Makefile
fi
# Patch Makefile.coqdocjs for pretty documentation targets
printf "\n# Include pretty documentation targets\ninclude scripts/coqdocjs/Makefile.coqdocjs" >> Makefile
# Patch HTML target to switch out color, and # Patch HTML target to switch out color, and
# so that it parses comments and has links to ssreflect. # so that it parses comments and has links to ssreflect.
# Also include Makefile.coqdocjs for 'htmlpretty' documentation target.
patch -s < scripts/Makefile.patch patch -s < scripts/Makefile.patch
...@@ -19,3 +19,13 @@ ...@@ -19,3 +19,13 @@
mlihtml: $(MLIFILES:.mli=.cmi) mlihtml: $(MLIFILES:.mli=.cmi)
$(SHOW)'CAMLDOC -d $@' $(SHOW)'CAMLDOC -d $@'
@@ -446,6 +449,9 @@
-toc $(COQDOCFLAGS) -pdf $(GAL) $(COQDOCLIBS) \
-o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
+# Prosa: include pretty documentation targets
+include scripts/coqdocjs/Makefile.coqdocjs
+
# FIXME: not quite right, since the output name is different
gallinahtml: GAL=-g
gallinahtml: html
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