diff --git a/tools/push-to-arduino.sh b/tools/push-to-arduino.sh index b8cf664b1..ff59889b1 100755 --- a/tools/push-to-arduino.sh +++ b/tools/push-to-arduino.sh @@ -1,16 +1,12 @@ #!/bin/bash -source ./tools/config.sh + +source ./tools/install-arduino.sh if [ -x $GITHUB_TOKEN ]; then echo "ERROR: GITHUB_TOKEN was not defined" exit 1 fi -if ! [ -d "$AR_COMPS/arduino" ]; then - echo "ERROR: Target arduino folder does not exist!" - exit 1 -fi - # setup git for pushing git config --global github.user "$GITHUB_ACTOR" git config --global user.name "$GITHUB_ACTOR"