From 7fc557a0e25d2d8f4e9bb20790578f9cef83097a Mon Sep 17 00:00:00 2001 From: Luca Heltai Date: Sun, 30 Apr 2023 13:24:51 +0000 Subject: [PATCH] Try to fix issue with indent. --- .github/workflows/docker.yml | 4 ++-- .github/workflows/indentation.yml | 1 + .github/workflows/tests.yml | 4 ++-- 3 files changed, 5 insertions(+), 4 deletions(-) diff --git a/.github/workflows/docker.yml b/.github/workflows/docker.yml index 410a5e453..deff41246 100644 --- a/.github/workflows/docker.yml +++ b/.github/workflows/docker.yml @@ -9,7 +9,7 @@ jobs: runs-on: ubuntu-latest steps: - name: Checkout code - uses: actions/checkout@v2 + uses: actions/checkout@v3 - name: Set up Docker Buildx uses: docker/setup-buildx-action@v1 @@ -21,7 +21,7 @@ jobs: password: ${{ secrets.DOCKER_PASSWORD }} - name: Build and push Docker image of master - uses: docker/build-push-action@v2 + uses: docker/build-push-action@v3 with: context: ./docker/ file: ./docker/Dockerfile.fsi-suite diff --git a/.github/workflows/indentation.yml b/.github/workflows/indentation.yml index d6cbda51d..4434f866e 100644 --- a/.github/workflows/indentation.yml +++ b/.github/workflows/indentation.yml @@ -25,4 +25,5 @@ jobs: fetch-depth: 100 - name: Check indentation run: | + git config --global --add safe.directory "$GITHUB_WORKSPACE" ./scripts/check_indentation.sh \ No newline at end of file diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index 564724d96..9be5d054d 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -15,7 +15,7 @@ jobs: options: --user root steps: - - uses: actions/checkout@v2 + - uses: actions/checkout@v3 - name: Build debug run: | rm -rf build_linux_debug @@ -38,7 +38,7 @@ jobs: options: --user root steps: - - uses: actions/checkout@v2 + - uses: actions/checkout@v3 - name: Build release run: | rm -rf build_linux_release