diff --git a/.github/push_database.sh b/.github/push_database.sh index 91a746c56..c90753f42 100755 --- a/.github/push_database.sh +++ b/.github/push_database.sh @@ -4,7 +4,7 @@ set -euo pipefail echo "Fetch unshallow" -git fetch --unshallow origin +git fetch --unshallow origin || true git stash CUR_BRANCH=$(git rev-parse --abbrev-ref HEAD)