diff options
| -rwxr-xr-x | tools/chbuild.sh | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/chbuild.sh b/tools/chbuild.sh index 94a6186..0340114 100755 --- a/tools/chbuild.sh +++ b/tools/chbuild.sh @@ -41,7 +41,7 @@ function chbuild { fi pushd $t > /dev/null printf "BUILDING: ${t}\n" - if [ -z "$CH_PATH" && -z "$CHC_PATH" ]; then + if [[ -z "$CH_PATH" && -z "$CHC_PATH" ]]; then make --quiet -j $JOBS > /dev/null else make CHIBIOS=$CH_PATH CHIBIOS_CONTRIB=$CHC_PATH --quiet -j $JOBS > /dev/null |