Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Rodolphe Lepigre
Iris
Commits
01b8c312
Commit
01b8c312
authored
Sep 19, 2017
by
Ralf Jung
Browse files
make build-dep: handle case where the pin already exists
parent
4be0320e
Changes
1
Hide whitespace changes
Inline
Side-by-side
Makefile
View file @
01b8c312
...
...
@@ -24,11 +24,13 @@ build-dep: phony
@
# To achieve this, we create a fake opam package that has our build-dependencies as
@
# dependencies, but does not actually install anything.
mkdir
-p
build-dep
@
echo
"build-dep package is
$$
BUILD_DEP_PACKAGE"
sed
<opam
's/^\(build\|install\|remove\):.*/\1: []/; s/^name: *"\(.*\)" */name: "\1-builddep"/'
>
build-dep/opam
@
sed
<opam
's/^\(build\|install\|remove\):.*/\1: []/; s/^name: *"\(.*\)" */name: "\1-builddep"/'
>
build-dep/opam
@
fgrep builddep build-dep/opam
>
/dev/null
||
(
echo
"sed failed to fix the package name"
&&
exit
1
)
# sanity check
@
# Compute the package name, add the pin and install it
opam pin add
"
$$
(egrep "
^name:
" build-dep/opam | sed 's/^name: *"
\(
.
*
\)
" */
\1
/')"
"
$
$(pwd)
/build-dep"
-k
path
$(OPAMFLAGS)
@
# Compute the package name, add the pin and
(
re
)
install
it. 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
/')"
;
\
opam pin add
"
$$
BUILD_DEP_PACKAGE"
"
$
$(pwd)
/build-dep"
-k
path
$(OPAMFLAGS)
&&
\
opam reinstall
"
$$
BUILD_DEP_PACKAGE"
# Some files that do *not* need to be forwarded to Makefile.coq
Makefile
:
;
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment