Commit e5889b23 authored by Ralf Jung's avatar Ralf Jung
Browse files

also add dev repos when using a beta

parent 39c267a4
......@@ -26,7 +26,7 @@ if [[ -z "$FRESH_OPAM" ]]; then # skip if this is a fresh opam root
# Make sure we got the right set of repositories registered
if echo "$@" | fgrep "dev" > /dev/null; then
if echo "$@" | egrep "(dev|beta)" > /dev/null; then
# We are compiling against a dev version of something. Get ourselves the dev repositories.
test -d "$OPAMROOT/repo/coq-extra-dev" || opam repo add coq-extra-dev -p 0
test -d "$OPAMROOT/repo/coq-core-dev" || opam repo add coq-core-dev -p 5
Supports Markdown
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