diff --git a/tools/check b/tools/check index d1a89e854c..537bcac2ca 100755 --- a/tools/check +++ b/tools/check @@ -291,7 +291,7 @@ run_icons() { run_shellcheck() { # Omitted from this check: nothing (nothing known, anyway). - files_check tools/ '!*.'{dart,js,json} \ + files_check tools/ '!*.'{dart,js,json} .envrc \ || return 0 # Shellcheck is fast, <1s; so if we touched any possible targets at all, @@ -300,6 +300,7 @@ run_shellcheck() { targets=( $(git grep -l '#!.*sh\b' -- tools/) $(git ls-files -- tools/'*.sh') + .envrc ) if ! type shellcheck >/dev/null 2>&1; then