From ec52f06c74fb6bbb9b6e97b25fb8c2196212f9b2 Mon Sep 17 00:00:00 2001
From: mattwparas <matthewparas2020@u.northwestern.edu>
Date: Fri, 22 Dec 2023 15:46:40 -0800
Subject: [PATCH] allow failure when moving directory in doc build

---
 .github/workflows/docs.yml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml
index 54b3d3145..c7e1f85de 100644
--- 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"