Merge pull request #12 from Pablo2048/development

Refuse to use GA :-(
This commit is contained in:
2024-10-12 15:35:10 +02:00
committed by GitHub

View File

@@ -1,27 +0,0 @@
name: Update Development Branch After PR Merge
on:
pull_request:
types: [closed]
jobs:
update-dev:
if: github.event.pull_request.merged == true && github.ref == 'refs/heads/main'
runs-on: ubuntu-latest
steps:
- name: Checkout repository
uses: actions/checkout@v2
with:
token: ${{ secrets.GITHUB_TOKEN }}
- name: Configure Git user
run: |
git config user.name "github-actions[bot]"
git config user.email "41898282+github-actions[bot]@users.noreply.github.com"
- name: Set executable permissions
run: chmod +x ./update_dev.sh
- name: Run update_dev.sh script
run: ./update_dev.sh