| commit | 34acd1d702e6b575f94ad9890626280db242bcb1 | [log] [tgz] |
|---|---|---|
| author | Davide Pesavento <davidepesa@gmail.com> | Sun Jul 21 13:45:02 2024 -0400 |
| committer | Davide Pesavento <davidepesa@gmail.com> | Sun Jul 21 13:45:02 2024 -0400 |
| tree | 85b8372680c51c419f56f589f3c8357bacd01ae6 | |
| parent | cf9feb44c485e7f9c60808bb95a189cce92939db [diff] [blame] |
Add .editorconfig Change-Id: Ifdb0d98f4e3011b70168644c86d9e225df749b15
diff --git a/.jenkins.d/00-deps.sh b/.jenkins.d/00-deps.sh index 9a2b436..59c90ef 100755 --- a/.jenkins.d/00-deps.sh +++ b/.jenkins.d/00-deps.sh
@@ -35,6 +35,7 @@ set -x if [[ $ID == macos ]]; then + export HOMEBREW_NO_ENV_HINTS=1 if [[ -n $GITHUB_ACTIONS ]]; then export HOMEBREW_NO_INSTALLED_DEPENDENTS_CHECK=1 fi