mirror of
https://github.com/erg-lang/erg.git
synced 2025-12-23 05:36:48 +00:00
Merge pull request #367 from toddlerer/add-sync_to_translation_status.er
This commit is contained in:
commit
db7e46b02f
28 changed files with 913 additions and 62 deletions
18
.github/workflows/docs.yml
vendored
18
.github/workflows/docs.yml
vendored
|
|
@ -2,12 +2,11 @@ name: Docs
|
|||
|
||||
on:
|
||||
push:
|
||||
branches: [main]
|
||||
paths:
|
||||
- "doc/**"
|
||||
|
||||
jobs:
|
||||
update-summary:
|
||||
automatic-update:
|
||||
runs-on: ubuntu-latest
|
||||
defaults:
|
||||
run:
|
||||
|
|
@ -17,11 +16,22 @@ jobs:
|
|||
- uses: actions/setup-python@v4
|
||||
with:
|
||||
python-version: "3.11"
|
||||
- run: |
|
||||
python sync_to_summary.py
|
||||
- uses: erg-lang/setup-erg@v2.1
|
||||
- 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
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue