Skip to content

Commit

Permalink
book: Publish both main and latest-release versions
Browse files Browse the repository at this point in the history
Also change the index to redirect to the latest release instead of `main`.
  • Loading branch information
nicholasbishop committed Jul 6, 2024
1 parent 4e4e190 commit 97e1c70
Show file tree
Hide file tree
Showing 3 changed files with 35 additions and 23 deletions.
42 changes: 27 additions & 15 deletions .github/workflows/book.yml
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@ name: Book
on:
push:
branches: [main]
tags: ['*']
permissions:
contents: write
# Adapted from:
Expand All @@ -21,24 +22,35 @@ jobs:
echo `pwd`/mdbook >> $GITHUB_PATH
- name: Deploy GitHub Pages
run: |
cd book
mdbook build
git worktree add gh-pages gh-pages
# Configure git user so that `git commit` works.
git config user.name "Deploy from CI"
git config user.email ""
cd gh-pages
# Get the highest `uefi` release tag.
highest_tag="$(git tag --list | grep uefi-v | sort -V | tail -1)"
# Create worktrees for both the `main` branch and the highest tag.
git worktree add --detach wt-main main
git worktree add --detach wt-tag "${highest_tag}"
# Create a worktree for the `gh-pages` branch.
git worktree add wt-gh-pages gh-pages
# Delete the ref to avoid keeping history.
git update-ref -d refs/heads/gh-pages
# Place the book under a "HEAD" directory so that we can later
# add other versions (e.g. "stable" or "v0.17") without breaking
# URLs.
rm -rf HEAD
mv ../book HEAD
git add HEAD
# Add an index in the root to redirect to HEAD. If we eventually
# serve multiple versions, this can be changed to a real index.
cp ../head_redirect.html index.html
git add index.html
git -C wt-gh-pages update-ref -d refs/heads/gh-pages
# Delete existing book builds.
rm -rf wt-gh-pages/HEAD wt-gh-pages/latest-release
# Build the book for both `main` and the highest tag.
mdbook build --dest-dir wt-gh-pages/HEAD wt-main/book
mdbook build --dest-dir wt-gh-pages/latest-release wt-tag/book
# Add an index in the root to redirect to the latest release.
cp wt-main/book/redirect.html wt-gh-pages/index.html
# Commit and push.
cd wt-gh-pages
git add HEAD latest-release index.html
git commit -m "Deploy $GITHUB_SHA to gh-pages"
git push --force
8 changes: 0 additions & 8 deletions book/head_redirect.html

This file was deleted.

8 changes: 8 additions & 0 deletions book/redirect.html
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
<!DOCTYPE html>
<head>
<meta charset="utf-8">
<title>Redirecting to latest release documentation</title>
<meta http-equiv="refresh" content="0; URL=latest-release">
</head>

Redirecting to <a href="latest-release">./latest-release</a>...

0 comments on commit 97e1c70

Please sign in to comment.