Skip to content

Merge pull request #517 from quatquatt/update-wiki-link #150

Merge pull request #517 from quatquatt/update-wiki-link

Merge pull request #517 from quatquatt/update-wiki-link #150

Workflow file for this run

name: Docs
on:
push:
branches: [main]
paths:
- "doc/**"
- "**.md"
jobs:
automatic-update:
if: github.repository_owner == 'erg-lang'
runs-on: ubuntu-latest
defaults:
run:
working-directory: doc
steps:
- uses: actions/checkout@v2
- uses: actions/setup-python@v4
with:
python-version: "3.11"
- run: pip install tqdm
- uses: erg-lang/[email protected]
- run: |
git config user.name github-actions[bot]
git config user.email 41898282+github-actions[bot]@users.noreply.github.com
- name: update summary
run: |
python scripts/sync_to_summary.py
git add .
git diff-index --quiet HEAD || git commit -m "Automatic update \`SUMMARY.md\`"
- name: update translation_status
run: |
erg --version
erg scripts/sync_to_translation_status.er
git add .
git diff-index --quiet HEAD || git commit -m "Automatic update \`translation_status\`"
- run: |
git push