allow failure when moving directory in doc build

mattwparas · Dec 22, 2023 · ec52f06 · ec52f06
1 parent 1c2846d
commit ec52f06
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml
@@ -32,12 +32,12 @@ jobs:
         # Delete the ref to avoid keeping history.
         git update-ref -d refs/heads/gh-pages
         # Delete everything except the book
-        mv dev/bench ..
+        mv dev/bench .. || true
         rm -rf *
         # There are benchmarks stored in dev/bench/ that we would like to
         # keep around. Otherwise, this just adds the book as a separate
         # directory.
-        mv ../dev/bench .
+        mv ../dev/bench . || true
         mv ../book/ .
         git add .
         git commit -m "Deploy $GITHUB_SHA to gh-pages"