[feature] Add some missing members (backport #5903) #5955
Workflow file for this run
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: conflicts | |
| on: | |
| pull_request: | |
| branches: ["2016", "2017", "2018", "2019", "2020", "2021", "2022"] | |
| types: [opened, reopened, synchronize, labeled] | |
| paths: ["src/**", "docs/**", ".github/**"] | |
| concurrency: | |
| group: ${{ github.workflow }}-${{ github.ref }} | |
| cancel-in-progress: true | |
| jobs: | |
| resolve: | |
| if: > | |
| contains(github.event.pull_request.labels.*.name, 'backport') && | |
| contains(github.event.pull_request.labels.*.name, 'conflicts') | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Set up Python | |
| uses: actions/setup-python@v5 | |
| with: | |
| python-version: "3.10" | |
| - uses: actions/checkout@v4 | |
| with: | |
| fetch-depth: 0 | |
| - name: Write pull request body to file | |
| uses: DamianReeves/write-file-action@v1.3 | |
| with: | |
| path: ${{ github.workspace }}/pull_request_body.txt | |
| contents: ${{ github.event.pull_request.body }} | |
| write-mode: overwrite | |
| - name: Delete deleted files | |
| run: | | |
| python ".github/scripts/conflicts.py" | |
| - name: Commit files | |
| run: | | |
| git config --local user.email "github-actions[bot]@users.noreply.github.com" | |
| git config --local user.name "github-actions[bot]" | |
| git commit -m "Delete conflicted deleted files by GitHub Action https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}" -a || true | |
| - name: Push changes | |
| uses: ad-m/github-push-action@v0.6.0 | |
| with: | |
| github_token: ${{ secrets.GITHUB_TOKEN }} | |
| branch: ${{ github.head_ref }} | |
| - name: Comment PR | |
| uses: Beakyn/gha-comment-pull-request@v1.0.2 | |
| env: | |
| GITHUB_TOKEN: ${{ github.token }} | |
| with: | |
| comment-message: | | |
| Hi @${{ github.event.pull_request.user.login }}, I have deleted the conflicted deleted files in this pull request. Please check it again. Thanks! | |
| delete-previous-comment: true |