1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
|
name: Deploy Docs
on:
push:
branches:
- stable
- master
# Builds all docs for both stable and master branches.
# In the gh-pages branch, we place:
# stable user-guide at /
# master user-guide at /devel
# master dev-guide at /dev-guide
jobs:
doc:
name: Documentation
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
with:
fetch-depth: 0
- name: Install mdbook
run: |
mkdir mdbook
curl -Lf https://github.com/rust-lang/mdBook/releases/download/v0.4.37/mdbook-v0.4.37-x86_64-unknown-linux-gnu.tar.gz | tar -xz --directory=./mdbook
echo "`pwd`/mdbook" >> $GITHUB_PATH
- name: Build book
run: |
# Build for stable
git checkout stable
# Support both old and new directory structure during the transition
cd doc/user-guide || cd doc
mdbook build
mv book ${{ runner.temp }}
# Build for master
cd $(git rev-parse --show-toplevel)
git checkout master
cd doc/user-guide
mdbook build
mv book ${{ runner.temp }}/book/devel
# Build dev-guide for master
cd ../dev-guide
mdbook build
mv book ${{ runner.temp }}/book/dev-guide
- name: Deploy to GitHub
run: |
cd ${{ runner.temp }}/book
git init
git config user.name "Deploy from CI"
git config user.email ""
git add . .nojekyll
git commit -m "Deploy $GITHUB_REF $GITHUB_SHA to gh-pages"
git remote add origin https://x-access-token:${{ secrets.GITHUB_TOKEN }}@github.com/$GITHUB_REPOSITORY
git push --force --set-upstream origin master:gh-pages
|
