diff --git a/jenkins/images.sh b/jenkins/images.sh index c651fb1b4c..d972b5dbba 100755 --- a/jenkins/images.sh +++ b/jenkins/images.sh @@ -133,6 +133,8 @@ set +x set +e echo "===================================================================" echo +export BOARD_A="${BOARD}" +export BOARD_B="${BOARD}" if [ "${GROUP}" != "developer" ]; then export CHANNEL_A="${GROUP}" else