Merge branch 'master' into dev

This commit is contained in:
Aliberk Sandıkçı 2025-01-20 21:29:34 +03:00
commit 4050729a8a

View file

@ -7,6 +7,7 @@ on:
- dev - dev
- master - master
- extended - extended
- '**-feature-**'
paths-ignore: paths-ignore:
- 'README.md' - 'README.md'
- 'doc/**' - 'doc/**'
@ -19,6 +20,7 @@ on:
branches: branches:
- dev - dev
- master - master
- extended
- '**-feature-**' - '**-feature-**'
paths-ignore: paths-ignore:
- 'README.md' - 'README.md'
@ -36,13 +38,9 @@ jobs:
permissions: write-all permissions: write-all
steps: steps:
- name: Checkout branch "${{ github.ref_name }}" - name: Checkout
env: uses: actions/checkout@v4
BRANCH: ${{ github.ref_name }}
run: |
git clone --no-checkout https://github.com/MaintainTeam/LastPipeBender.git .
git checkout --progress --force "$BRANCH"
- name: Set up JDK - name: Set up JDK
uses: actions/setup-java@v4 uses: actions/setup-java@v4
with: with: