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
Dmitry Khalanskiy
Iris
Commits
b6d476bf
Commit
b6d476bf
authored
Oct 10, 2017
by
Ralf Jung
Browse files
have Coq's dev repos only for dev builds
parent
6ed8faa8
Changes
1
Hide whitespace changes
Inline
Side-by-side
build/opam-ci.sh
View file @
b6d476bf
...
...
@@ -20,7 +20,7 @@ run_and_print opam pin remove coq-iris -n
# Make sure the pin for the builddep package is not stale.
run_and_print make build-dep/opam
#
Get us all the l
ate
st
repositories
#
Upd
ate repositories
if
test
$(
find
"
$OPAMROOT
/repo/package-index"
-mtime
+0
)
;
then
# last update was more than a day ago
run_and_print opam update
...
...
@@ -28,8 +28,16 @@ else
# only update iris-dev
if
test
-d
"
$OPAMROOT
/repo/iris-dev"
;
then
run_and_print opam update iris-dev
;
fi
fi
test
-d
"
$OPAMROOT
/repo/coq-extra-dev"
&&
run_and_print opam repo remove coq-extra-dev
test
-d
"
$OPAMROOT
/repo/coq-core-dev"
||
run_and_print opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev
-p
5
# Make sure we got the right set of repositories registered
if
echo
"
$@
"
| fgrep
"dev"
;
then
# We are compiling against a dev version of something. Get ourselves the dev repositories.
test
-d
"
$OPAMROOT
/repo/coq-extra-dev"
||
run_and_print opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev
-p
0
test
-d
"
$OPAMROOT
/repo/coq-core-dev"
||
run_and_print opam repo add coq-core-dev https://coq.inria.fr/opam/core-dev
-p
5
else
# No dev version, make sure we do not have the dev repositories.
test
-d
"
$OPAMROOT
/repo/coq-extra-dev"
&&
run_and_print opam repo remove coq-extra-dev
test
-d
"
$OPAMROOT
/repo/coq-core-dev"
&&
run_and_print opam repo remove coq-core-dev
fi
test
-d
"
$OPAMROOT
/repo/coq-released"
||
run_and_print opam repo add coq-released https://coq.inria.fr/opam/released
-p
10
test
-d
"
$OPAMROOT
/repo/iris-dev"
||
run_and_print opam repo add iris-dev https://gitlab.mpi-sws.org/FP/opam-dev.git
-p
20
echo
...
...
@@ -48,7 +56,7 @@ while (( "$#" )); do # while there are arguments left
echo
"[opam-ci]
$PACKAGE
already pinned to
$VERSION
"
else
echo
"[opam-ci] Pinning
$PACKAGE
to
$VERSION
"
run_and_print opam pin add
"
$PACKAGE
"
"
$VERSION
"
-k
version
-y
run_and_print opam pin add
-y
-k
version
"
$PACKAGE
"
"
$VERSION
"
fi
done
...
...
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