Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Iris
ci
Commits
a0695a43
Commit
a0695a43
authored
Sep 26, 2020
by
Ralf Jung
Browse files
Support repositories with mutliple opam files
parent
697e472e
Changes
1
Hide whitespace changes
Inline
Side-by-side
prepare-opam.sh
View file @
a0695a43
...
...
@@ -48,12 +48,18 @@ test -d "$OPAMROOT/repo/iris-dev" || opam repo add iris-dev https://gitlab.mpi-s
opam repo prio iris-dev 1
# make sure this stays at the top
echo
# Make sure the the builddep package exists and is up-to-date.
make build-dep/opam
# Make sure the the builddep package(s) exist and are up-to-date.
if
test
-f
opam
;
then
# Old-style package: a single opam file
make build-dep/opam
else
# New-style package has a dedicated target to just generate the files
make build-dep-opamfiles
fi
# Update old opam, if we got a cache.
if
[[
-z
"
$FRESH_OPAM
"
]]
;
then
# skip if this is a fresh opam root
# Update repositories and reinit. build-dep/
opam
must exist here because it
# Update repositories and reinit. build-dep/
*
must exist here because it
# might be installed, and opam would complain if it had went missing.
opam init
--no-setup
--disable-sandboxing
--reinit
-y
# We need `opam update` anyway to update git branches.
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a 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