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

update Makefile

parent e9312c57
No related branches found
No related tags found
No related merge requests found
Pipeline #14449 canceled
...@@ -28,16 +28,15 @@ build-dep: build-dep/opam phony ...@@ -28,16 +28,15 @@ build-dep: build-dep/opam phony
@# constraints. Otherwise, `opam upgrade` may well update some packages to versions @# constraints. Otherwise, `opam upgrade` may well update some packages to versions
@# that are incompatible with our build requirements. @# that are incompatible with our build requirements.
@# To achieve this, we create a fake opam package that has our build-dependencies as @# To achieve this, we create a fake opam package that has our build-dependencies as
@# dependencies, but does not actually install anything. @# dependencies, but does not actually install anything itself.
@# Reinstalling is needed with opam 1 in case the pin already exists, but the builddep @echo "# Pinning build-dep package." && \
@# package changed. if opam --version | grep "^1\." -q; then \
@BUILD_DEP_PACKAGE="$$(egrep "^name:" build-dep/opam | sed 's/^name: *"\(.*\)" */\1/')" && \ BUILD_DEP_PACKAGE="$$(egrep "^name:" build-dep/opam | sed 's/^name: *"\(.*\)" */\1/')" && \
echo "# Pinning build-dep package." && \ opam pin add -k path $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE".dev build-dep && \
opam pin add -k path $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE".dev build-dep && \ opam reinstall $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE"; \
((! opam --version | grep "^1\." > /dev/null) || ( \ else \
echo "# Reinstalling build-dep package." && \ opam install $(OPAMFLAGS) build-dep/; \
opam reinstall $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE" \ fi
))
# Some files that do *not* need to be forwarded to Makefile.coq # Some files that do *not* need to be forwarded to Makefile.coq
Makefile: ; Makefile: ;
......
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