diff options
author | Ben Gamari <ben@smart-cactus.org> | 2021-10-03 14:23:45 -0400 |
---|---|---|
committer | Ben Gamari <ben@smart-cactus.org> | 2021-10-03 14:23:45 -0400 |
commit | 91cd124843d3c03639ec12a62b2b43d9b45a8d52 (patch) | |
tree | 8c13e4cdaa10c7bb9170dd100a3f2c18fd3d195d /.gitlab | |
parent | f4554f1d2a5684042484c38ed831a2b93536b9c6 (diff) | |
download | haskell-91cd124843d3c03639ec12a62b2b43d9b45a8d52.tar.gz |
ci/test-metrics: Clean up various bash quoting issues
Diffstat (limited to '.gitlab')
-rwxr-xr-x | .gitlab/test-metrics.sh | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/.gitlab/test-metrics.sh b/.gitlab/test-metrics.sh index fe16573672..8d67ee7cee 100755 --- a/.gitlab/test-metrics.sh +++ b/.gitlab/test-metrics.sh @@ -17,7 +17,7 @@ fail() { function pull() { local ref="refs/notes/$REF" - run git fetch -f $NOTES_ORIGIN $ref:$ref + run git fetch -f "$NOTES_ORIGIN" "$ref:$ref" echo "perf notes ref $ref is $(git rev-parse $ref)" } @@ -25,8 +25,8 @@ function pull() { # This is favoured over a git notes merge as it avoids potential data loss/duplication from the merge strategy. function reset_append_note_push { pull || true - run git notes --ref=$REF append -F $METRICS_FILE HEAD - run git push $PERF_NOTES_PUSH_REPO refs/notes/$REF + run git notes --ref="$REF" append -F "$METRICS_FILE" HEAD + run git push "$PERF_NOTES_PUSH_REPO" "refs/notes/$REF" } function push() { @@ -41,17 +41,17 @@ function push() { fi # TEST_ENV must be set. - if [ -z ${TEST_ENV+"$TEST_ENV"} ] + if [ -z "${TEST_ENV:-}" ] then fail "Not pushing performance git notes: TEST_ENV must be set." fi # Assert that the METRICS_FILE exists and can be read. - if [ -z ${METRICS_FILE+"$METRICS_FILE"} ] + if [ -z "${METRICS_FILE:-}" ] then fail "\$METRICS_FILE not set." fi - if ! [ -r $METRICS_FILE ] + if ! [ -r "$METRICS_FILE" ] then fail "Metrics file not found: $METRICS_FILE" fi |