@@ -2,6 +2,7 @@ name: Book
2
2
on :
3
3
push :
4
4
branches : [main]
5
+ tags : ['*']
5
6
permissions :
6
7
contents : write
7
8
# Adapted from:
@@ -21,24 +22,32 @@ jobs:
21
22
echo `pwd`/mdbook >> $GITHUB_PATH
22
23
- name : Deploy GitHub Pages
23
24
run : |
24
- cd book
25
- mdbook build
26
- git worktree add gh-pages gh-pages
25
+ # Configure git user so that `git commit` works.
27
26
git config user.name "Deploy from CI"
28
27
git config user.email ""
29
- cd gh-pages
28
+
29
+ # Get the highest `uefi` release tag.
30
+ highest_tag="$(git tag --list | grep uefi-v | sort -V | tail -1)"
31
+
32
+ # Create a worktree for the tag.
33
+ git worktree add wt-tag refs/tags/"${highest_tag}"
34
+
35
+ # Create a worktree for the `gh-pages` branch.
36
+ git worktree add wt-gh-pages gh-pages
37
+
30
38
# Delete the ref to avoid keeping history.
31
- git update-ref -d refs/heads/gh-pages
32
- # Place the book under a "HEAD" directory so that we can later
33
- # add other versions (e.g. "stable" or "v0.17") without breaking
34
- # URLs.
35
- rm -rf HEAD
36
- mv ../book HEAD
37
- git add HEAD
38
- # Add an index in the root to redirect to HEAD. If we eventually
39
- # serve multiple versions, this can be changed to a real index.
40
- cp ../head_redirect.html index.html
41
- git add index.html
39
+ git -C wt-gh-pages update-ref -d refs/heads/gh-pages
40
+
41
+ # Build the book for the tag. Don't use `--dest-dir` because it will
42
+ # delete the destination directory including the worktree checkout's
43
+ # ".git".
44
+ mdbook build wt-tag/book
45
+ # Copy output to the destination directory. Note the "/." is needed at
46
+ # the end of the source path so that hidden files are included.
47
+ cp -r wt-tag/book/book/. wt-gh-pages
48
+
42
49
# Commit and push.
50
+ cd wt-gh-pages
51
+ git add .
43
52
git commit -m "Deploy $GITHUB_SHA to gh-pages"
44
53
git push --force
0 commit comments