Skip to content
Snippets Groups Projects
Commit 57e1431e authored by Ralf Jung's avatar Ralf Jung
Browse files

fix make build-dep

parent 7d67e4d7
No related branches found
No related tags found
No related merge requests found
Pipeline #
Hide whitespace changes
Inline Side-by-side
Showing
with 1 addition and 1 deletion
Makefile
+ 1
− 1
View file @ 57e1431e
...@@ -29,7 +29,7 @@ build-dep: phony ...@@ -29,7 +29,7 @@ build-dep: phony
@fgrep builddep build-dep/opam >/dev/null || (echo "sed failed to fix the package name" && exit 1) # sanity check @fgrep builddep build-dep/opam >/dev/null || (echo "sed failed to fix the package name" && exit 1) # sanity check
@# Reinstallation is needed in case the pin already exists, but the builddep package changed. @# Reinstallation is needed in case the pin already exists, but the builddep package changed.
@BUILD_DEP_PACKAGE="$$(egrep "^name:" build-dep/opam | sed 's/^name: *"\(.*\)" */\1/')"; \ @BUILD_DEP_PACKAGE="$$(egrep "^name:" build-dep/opam | sed 's/^name: *"\(.*\)" */\1/')"; \
opam pin add "$$BUILD_DEP_PACKAGE" "$$(pwd)/build-dep" -k path $(OPAMFLAGS) && \ opam pin add "$$BUILD_DEP_PACKAGE".dev "$$(pwd)/build-dep" -k path $(OPAMFLAGS) && \
opam reinstall "$$BUILD_DEP_PACKAGE" opam reinstall "$$BUILD_DEP_PACKAGE"
# Some files that do *not* need to be forwarded to Makefile.coq # Some files that do *not* need to be forwarded to Makefile.coq
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment