diff options
| author | Enrico Tassi | 2020-12-14 12:01:29 +0100 |
|---|---|---|
| committer | GitHub | 2020-12-14 12:01:29 +0100 |
| commit | 477cba2c8906c2007b6aa6c9aa2b352d096ec844 (patch) | |
| tree | 4bc3248e82f8c24faf3e34c201f1fc63847e2244 /dev | |
| parent | 8817a18edc9185891d48e0da9e214a678fb97b75 (diff) | |
Update dev/tools/pin-ci.sh
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Diffstat (limited to 'dev')
| -rwxr-xr-x | dev/tools/pin-ci.sh | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/tools/pin-ci.sh b/dev/tools/pin-ci.sh index a1ee83a004..676688bedc 100755 --- a/dev/tools/pin-ci.sh +++ b/dev/tools/pin-ci.sh @@ -38,7 +38,7 @@ process_development() { # Execute the script to set the overlay variables . $OVERLAYS -for project in ${projects[*]} +for project in ${projects[@]} do process_development $project done |