Skip to content

Commit 5c4ebe0

Browse files
committed
Automatically generate documentation for hosting via Github Pages
In addition to the extensive header documentation available lets also have doxygen generate proper HTML for the web.
1 parent f577951 commit 5c4ebe0

File tree

1 file changed

+84
-0
lines changed

1 file changed

+84
-0
lines changed
Lines changed: 84 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,84 @@
1+
name: Generate Documentation
2+
3+
on:
4+
push:
5+
branches:
6+
- '*'
7+
- '!documentation'
8+
paths:
9+
- '.github/workflows/documentation.yml'
10+
- 'LICENSE'
11+
12+
jobs:
13+
docs:
14+
name: "Generate Documentation"
15+
runs-on: ubuntu-latest
16+
steps:
17+
- name: "Set up Git"
18+
shell: bash
19+
run: |
20+
git config --global user.name 'GitHub Actions'
21+
git config --global user.email 'xaymar@users.noreply.github.com'
22+
git config --global pull.ff only
23+
git config --global pull.rebase true
24+
25+
- name: "Clone"
26+
uses: actions/checkout@v3
27+
with:
28+
submodules: 'recursive'
29+
fetch-depth: 0
30+
31+
- name: "Clone Documentation Cache"
32+
id: doc_cache
33+
continue-on-error: true
34+
uses: actions/checkout@v3
35+
with:
36+
ref: 'documentation'
37+
path: 'build/docs/html'
38+
submodules: 'recursive'
39+
fetch-depth: 0
40+
41+
- name: "Initialize Documentation Cache"
42+
if: steps.doc_cache.outcome == 'failure'
43+
shell: bash
44+
run: |
45+
mkdir -p build/docs/html
46+
pushd build/docs/html
47+
git init
48+
git switch --orphan documentation
49+
git remote remove origin
50+
git remote add -t documentation origin ${{ github.repositoryUrl }}
51+
popd
52+
53+
- name: "Install Prerequisites"
54+
shell: bash
55+
run: |
56+
sudo apt-get install -y clang-19 clang-tools-19 doxygen graphviz
57+
58+
- name: "Generate Documentation"
59+
shell: bash
60+
run: |
61+
doxygen Doxyfile
62+
63+
- name: "Update Documentation"
64+
shell: bash
65+
run: |
66+
pushd build/docs/html
67+
git add .
68+
git --no-pager diff --patch --minimal HEAD --
69+
git update-index --refresh
70+
if ! git diff-index --quiet HEAD --; then
71+
git commit -a -m "${{ github.sha }}"
72+
73+
# Only push from master branch.
74+
if [[ "${{ github.ref }}" == "refs/heads/master" ]]; then
75+
git push
76+
echo "Documentation has been updated!"
77+
else
78+
git log --graph --pretty=format:'%Cred%h%Creset -%C(yellow)%d%Creset %s %Cgreen(%cr) %C(bold blue)<%an>%Creset' --abbrev-commit
79+
fi
80+
else
81+
echo "Documentation is still up to date."
82+
fi
83+
popd
84+

0 commit comments

Comments
 (0)