From 0191c760970c83ae015c856775a7dbf993d15d60 Mon Sep 17 00:00:00 2001
From: Adam Turner <9087854+aa-turner@users.noreply.github.com>
Date: Sat, 12 Apr 2025 00:13:35 +0100
Subject: [PATCH] Ensure that `Doc/dist` exists

---
 build_docs.py | 1 +
 1 file changed, 1 insertion(+)

diff --git a/build_docs.py b/build_docs.py
index 309d786..f47b0e3 100755
--- a/build_docs.py
+++ b/build_docs.py
@@ -802,6 +802,7 @@ def copy_build_to_webroot(self, http: urllib3.PoolManager) -> None:
         if not self.quick:
             # Copy archive files to /archives/
             logging.debug("Copying dist files.")
+            (self.checkout / "Doc" / "dist").mkdir(exist_ok=True)
             run([
                 "chown",
                 "-R",