diff options
Diffstat (limited to '.github')
| -rw-r--r-- | .github/workflows/docs.yaml | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/.github/workflows/docs.yaml b/.github/workflows/docs.yaml index 22a2d4f6bf..808f825331 100644 --- a/.github/workflows/docs.yaml +++ b/.github/workflows/docs.yaml @@ -25,7 +25,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 # Figure out the target directory. # |