Generate Manual #41
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
--- | |
name: Generate Manual | |
on: | |
push: | |
paths: | |
- 'docs/src/manual.md' | |
workflow_dispatch: | |
jobs: | |
gen_man: | |
permissions: | |
contents: write | |
runs-on: ubuntu-latest | |
steps: | |
- uses: actions/checkout@v3 | |
- id: generate | |
run: | | |
sudo apt-get update | |
sudo apt-get install pandoc | |
./man/gen-man | |
- name: push updated manual | |
run: | | |
git config --global user.name denv-docs-bot | |
git config --global user.email [email protected] | |
git switch -c auto-man-update | |
git add man | |
git commit -m "Auto Man Page Update from ${{ github.event.head_commit.message }}" || exit 0 | |
gh pr create --fill | |
env: | |
GH_TOKEN: ${{ github.token }} |