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
name: Update Library Documentation
on:
# Run on pushes to master that change library source files
push:
branches:
paths:
- 'src/syntax/library/**'
- 'scripts/generate-library-docs.py'
# Allow manual trigger
workflow_dispatch:
jobs:
library:
runs-on: ubuntu-latest
steps:
- name: Checkout repository
uses: actions/checkout@v4
- name: Install Python
uses: actions/setup-python@v4
with:
python-version: '3.x'
- name: Install Python dependencies
run: pip install markdown
- name: Generate library documentation
run: |
chmod +x ./scripts/generate-library-docs.py
python3 ./scripts/generate-library-docs.py --clean
- name: Commit and push if changed
run: |
git pull
git config --global user.name 'github-actions[bot]'
git config --global user.email 'github-actions[bot]@users.noreply.github.com'
git add docs/library/
if git diff --staged --quiet; then
echo "No changes to commit"
else
git commit -m "Update library documentation [skip ci]"
git push
fi