summary refs log tree commit diff
path: root/.github
diff options
context:
space:
mode:
Diffstat (limited to '.github')
-rw-r--r--.github/workflows/docs.yaml7
1 files changed, 6 insertions, 1 deletions
diff --git a/.github/workflows/docs.yaml b/.github/workflows/docs.yaml
index 23b8d7f909..c239130c57 100644
--- a/.github/workflows/docs.yaml
+++ b/.github/workflows/docs.yaml
@@ -23,7 +23,12 @@ jobs:
           mdbook-version: '0.4.9'
 
       - name: Build the documentation
-        run: mdbook build
+        # mdbook will only create an index.html if we're including docs/README.md in SUMMARY.md.
+        # However, we're using docs/README.md for other purposes and need to pick a new page
+        # as the default. Let's opt for the welcome page instead.
+        run: |
+          mdbook build
+          cp book/welcome_and_overview.html book/index.html
 
       # Deploy to the latest documentation directories
       - name: Deploy latest documentation