Skip to content

Commit

Permalink
tests/run.sh: use $* to concatenate
Browse files Browse the repository at this point in the history
In bash `$@` is an array. Doing `x=$@` is assigning an array to a
string. Different shells handle this differently. `$*` is explicit about
wanting to concatenate the array to a list which is the behavior we are
currently relying on.

https://www.shellcheck.net/wiki/SC2124
  • Loading branch information
erooke committed Dec 5, 2024
1 parent 293959b commit c42eaf5
Showing 1 changed file with 3 additions and 3 deletions.
6 changes: 3 additions & 3 deletions tests/run.sh
Original file line number Diff line number Diff line change
Expand Up @@ -47,7 +47,7 @@ fi


shift
k2_args="$@"
k2_args="$*"

basic_k2_cmd="$k2_args --color false --check_subproperties true --check_sat_assume false --enforce_func_congruence true"

Expand Down Expand Up @@ -93,7 +93,7 @@ function run_one {
shift
expected_code="$1"
shift
full_kind2_cmd="$@ $file_path"
full_kind2_cmd="$* $file_path"
expected_code_str=$(str_of_code "$expected_code")

printf "| %-40s ... " "$(name_of_path "$file_path")"
Expand Down Expand Up @@ -123,7 +123,7 @@ function find_tests {
function run_in {
work_dir="$1"
shift
kind2_cmd="$@"
kind2_cmd="$*"
# Falsifiable
find_cmd=$(find_tests "$work_dir" $falsifiable_dir)
file_count=$(eval "$find_cmd" | wc -l | tr -d ' ')
Expand Down

0 comments on commit c42eaf5

Please sign in to comment.