Merge branch 'develop' into feature/jdk21

2026-08-17 04:36:02 +00:00 · 2023-10-16 16:12:10 +02:00
parent 83879f5cfe 2d503a0edb
commit 162ebf6545
12 changed files with 28 additions and 19 deletions
@@ -17,7 +17,7 @@ jobs:
    runs-on: ubuntu-latest
    if: "!contains(github.event.head_commit.message, '[ci skip]') && !contains(github.event.head_commit.message, '[skip ci]')"
    steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
      - uses: actions/setup-java@v3
        with:
          distribution: ${{ env.JAVA_DIST }}