Skip to content

[wiki] Publish merged docs to wiki master (#48) #50

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
coisa merged 3 commits into from
Apr 17, 2026
Merged

[wiki] Publish merged docs to wiki master (#48) #50

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
5f2d974
Fix wiki publish branch
coisa Apr 17, 2026
9cf0df1
Update wiki submodule pointer for PR #50
github-actions[bot] Apr 17, 2026
72d0984
Delete published wiki preview branch
coisa Apr 17, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion .github/wiki
Open in desktop
Submodule wiki updated from aef19f to 27c2a1
17 changes: 11 additions & 6 deletions .github/workflows/wiki.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -112,11 +112,12 @@ jobs:
push: true

publish:
name: Publish Wiki Main
name: Publish Wiki Master
if: github.event_name == 'pull_request_target' && github.event.pull_request.merged == true && github.event.pull_request.base.ref == 'main'
runs-on: ubuntu-latest

env:
WIKI_PUBLISH_BRANCH: master
WIKI_PREVIEW_BRANCH: pr-${{ github.event.pull_request.number }}

steps:
Expand All @@ -133,19 +134,23 @@ jobs:
git config --global --add safe.directory "$GITHUB_WORKSPACE"
git config --global --add safe.directory "$GITHUB_WORKSPACE/.github/wiki"

- name: Prepare wiki main branch from preview branch
- name: Prepare wiki publish branch from preview branch
working-directory: .github/wiki
run: |
git fetch origin main "${WIKI_PREVIEW_BRANCH}"
git switch -C main --track origin/main || git switch main
git fetch origin "${WIKI_PUBLISH_BRANCH}" "${WIKI_PREVIEW_BRANCH}"
git switch -C "${WIKI_PUBLISH_BRANCH}" --track "origin/${WIKI_PUBLISH_BRANCH}" || git switch "${WIKI_PUBLISH_BRANCH}"
git reset --hard "origin/${WIKI_PREVIEW_BRANCH}"
git clean -fd

- name: Commit & push wiki main branch
- name: Commit & push wiki publish branch
Comment thread
coisa marked this conversation as resolved.
Dismissed
uses: EndBug/add-and-commit@v10
with:
cwd: .github/wiki
add: .
message: "Publish wiki docs from PR #${{ github.event.pull_request.number }}"
default_author: github_actions
push: origin HEAD:main
push: origin HEAD:${{ env.WIKI_PUBLISH_BRANCH }}

- name: Delete wiki preview branch
working-directory: .github/wiki
run: git push origin --delete "${WIKI_PREVIEW_BRANCH}"
Loading