File tree Expand file tree Collapse file tree
Expand file tree Collapse file tree Original file line number Diff line number Diff line change 1+ ---
2+ name : Convert markdown docs to html
3+
4+ on :
5+ push :
6+ branches : ["master", "develop"]
7+ paths :
8+ - proposal/**
9+ - .github/workflows/build-docs.yml
10+
11+ workflow_dispatch :
12+
13+ concurrency :
14+ group : ${{ github.workflow }}-${{ github.ref }}
15+ cancel-in-progress : false
16+
17+ jobs :
18+ deploy :
19+ runs-on : ubuntu-latest
20+ container :
21+ image : cppalliance/wg21:latest
22+ options : --user 1001
23+
24+ steps :
25+ - name : Checkout
26+ uses : actions/checkout@v4
27+ - name : Build docs
28+ run : |
29+ set -xe
30+ # list_of_files="draft P3390R0"
31+ list_of_files="draft"
32+ cd proposal
33+ git clone https://github.com/mpark/wg21.git
34+ echo "include wg21/Makefile" > Makefile
35+ for file in $list_of_files; do
36+ make ${file}.html
37+ done
38+ cp generated/* ../docs/
39+ cd ..
40+ git config --global user.name 'commitbot'
41+ git config --global user.email 'commitbot@boost.org'
42+ git add docs/* || true
43+ git commit -m "Docs: update from proposal/ md files" || true
44+ git push
45+
46+ - name : Trigger Publish Workflow
47+ uses : actions/github-script@v7
48+ with :
49+ script : |
50+ github.rest.repos.createDispatchEvent({
51+ owner: context.repo.owner,
52+ repo: context.repo.repo,
53+ event_type: 'publish-trigger',
54+ });
Original file line number Diff line number Diff line change 1111 # Allows you to run this workflow manually from the Actions tab
1212 workflow_dispatch :
1313
14+ repository_dispatch :
15+ types : [publish-trigger]
16+
1417# Sets permissions of the GITHUB_TOKEN to allow deployment to GitHub Pages
1518permissions :
1619 contents : read
You can’t perform that action at this time.
0 commit comments