diff options
Diffstat (limited to 'dev/ci/ci-basic-overlay.sh')
| -rwxr-xr-x | dev/ci/ci-basic-overlay.sh | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index b65430aa51..8bcbd90f0b 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -7,11 +7,10 @@ declare -a projects # the list of project repos that can be be overlayed # checks if the given argument is a known project function is_in_projects { - local rc=1 - for x in ${projects[@]}; do - if [ "$1" = "$x" ]; then rc=0; fi; + for x in "${projects[@]}"; do + if [ "$1" = "$x" ]; then return 0; fi; done - return rc + return 1 } # project <name> <giturl> <ref> [<archiveurl>] @@ -102,7 +101,7 @@ project geocoq "https://github.com/GeoCoq/GeoCoq" "master" ######################################################################## # Flocq ######################################################################## -project flocq "https://gitlab.inria.fr/flocq/flocq" "master" +project flocq "https://gitlab.inria.fr/flocq/flocq" "flocq-3" ######################################################################## # coq-performance-tests |