diff --git a/.github/kokoro/db-full.sh b/.github/kokoro/db-full.sh index 0e3627ea..1b8d91f1 100755 --- a/.github/kokoro/db-full.sh +++ b/.github/kokoro/db-full.sh @@ -44,7 +44,7 @@ echo "----------------------------------------" echo "----------------------------------------" export MAX_VIVADO_PROCESS=$CORES set -x - make -j $CORES MAX_VIVADO_PROCESS=$CORES + script --return --flush --command "make -j $CORES MAX_VIVADO_PROCESS=$CORES" - set +x echo "----------------------------------------" echo "make --dry-run" diff --git a/.github/kokoro/db-quick.sh b/.github/kokoro/db-quick.sh index 58e0f69b..13c91e10 100755 --- a/.github/kokoro/db-quick.sh +++ b/.github/kokoro/db-quick.sh @@ -34,7 +34,7 @@ echo "----------------------------------------" echo "----------------------------------------" export MAX_VIVADO_PROCESS=$CORES set -x - make -j $CORES MAX_VIVADO_PROCESS=$CORES QUICK=y + script --return --flush --command "make -j $CORES MAX_VIVADO_PROCESS=$CORES QUICK=y" - set +x ) echo "----------------------------------------"