blob: 1f69ba0d635c9e7c15c3e783673117789b028da1 (
plain)
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
|
name: docs
on:
push:
tags:
- v[0-9]+.[0-9]+.[0-9]+
branches:
- main
jobs:
docs:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v2
- name: configure git
run: |
git config user.name "${GITHUB_ACTOR}"
git config user.email "${GITHUB_ACTOR}@bots.github.com"
git fetch --no-tags --prune --depth=1 origin +refs/heads/*:refs/remotes/origin/*
- name: Set up Python
uses: actions/setup-python@v2
with:
python-version: "3.7"
- name: Install dependencies
run: make doc-setup
- name: Build docs
run: make doc
- name: commit docs
run: |
git checkout gh-pages
rm -rf $(basename ${GITHUB_REF})
mv docs/_build/html $(basename ${GITHUB_REF})
git show origin/main:docs/_gh_include/header.inc > index.html
(echo main; dirname v*/index.html | sort --version-sort --reverse) | xargs -I@@ -n1 echo '<div class="col-md-4 center"><a href="@@/" class="btn-doc btn"><i class="fa fa-newspaper-o"></i><p>@@</p></a></div>' >> index.html
git show origin/main:docs/_gh_include/footer.inc >> index.html
git add $(basename ${GITHUB_REF}) index.html
git commit -m "update docs for $(basename ${GITHUB_REF})" || true
- name: push docs
run: git push origin gh-pages
|
