File tree Expand file tree Collapse file tree
Expand file tree Collapse file tree Original file line number Diff line number Diff line change 2727 gh api -H 'Accept: application/vnd.github.raw' '/repos/leanprover/vscode-lean4/contents/lean4-unicode-input/src/abbreviations.json' >vscode-lean/abbreviations.json
2828 env :
2929 GITHUB_TOKEN : ${{ secrets.GITHUB_TOKEN }}
30- - uses : stefanzweifel/git-auto-commit-action@04702edda442b2e678b25b537cec683a1493fcb9
31- with :
32- commit_message : Sync abbreviations with the VSCode definitions
30+ - name : Commit
31+ run : |
32+ git config user.name "github-actions[bot]"
33+ git config user.email "41898282+github-actions[bot]@users.noreply.github.com"
34+ git add -A
35+ if ! git diff --staged --quiet; then
36+ git commit -m "Sync abbreviations with the VSCode definitions"
37+ git push
38+ fi
Original file line number Diff line number Diff line change 3939 run : just docs
4040
4141 - name : Commit
42- uses : stefanzweifel/git-auto-commit-action@04702edda442b2e678b25b537cec683a1493fcb9
43- with :
44- branch : ${{ github.head_ref }}
45- commit_message : " Regenerate vimdocs"
46- file_pattern : doc/*.txt
42+ run : |
43+ git config user.name "github-actions[bot]"
44+ git config user.email "41898282+github-actions[bot]@users.noreply.github.com"
45+ git add doc/*.txt
46+ if ! git diff --staged --quiet; then
47+ git commit -m "Regenerate vimdocs"
48+ git push
49+ fi
You can’t perform that action at this time.
0 commit comments