fix: update docs

obreitwi · May 27, 2024 · f870ce4 · f870ce4
1 parent f635302
commit f870ce4
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/tools/update-docs-HEAD.sh b/tools/update-docs-HEAD.sh
@@ -32,7 +32,7 @@ upload_docs()
 {
  git push "${remote}" :gh-pages
  git fetch "${remote}"
- git branch -D gh-pages
+ git branch -D gh-pages || true
  ghp-import --force \
  --push \
  --no-jekyll \