diff options
| author | Enrico Tassi | 2020-12-14 11:01:14 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2020-12-14 11:01:14 +0100 |
| commit | c95058a0f70608c82195f34fef78ac50d517cf8a (patch) | |
| tree | af4011d8b7f09fa992dd6edd7099a3b3c4f58e74 /dev/ci | |
| parent | d0667eb4a165c065b0d64069641ca0cd39d62219 (diff) | |
[ci] fix code to check if the overlay is valid
Diffstat (limited to 'dev/ci')
| -rwxr-xr-x | dev/ci/ci-basic-overlay.sh | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index be819616e2..dd683c96a9 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -8,7 +8,7 @@ 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 + for x in ${projects[@]}; do if [ "$1" = "$x" ]; then rc=0; fi; done return rc |
