From 013c01059ef9148a1f3b673d556cd5e423cb1038 Mon Sep 17 00:00:00 2001
From: Stefan van der Walt <stefanv@berkeley.edu>
Date: Fri, 11 Sep 2026 23:32:15 +0000
Subject: [PATCH] Do not fail if the dev directory survives the removal

---
 .github/workflows/publish_docs_to_pages.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/publish_docs_to_pages.yml b/.github/workflows/publish_docs_to_pages.yml
index cea91ac..5eb67ae 100644
--- a/.github/workflows/publish_docs_to_pages.yml
+++ b/.github/workflows/publish_docs_to_pages.yml
@@ -44,7 +44,7 @@ jobs:
         cd ..
         echo "Committing emptied dev directory"
         git commit -m "Remove old dev documentation"
-        mkdir dev
+        mkdir -p dev
         cd dev
         echo "Copying /tmp/html here"
         cp -v -r /tmp/html/* .