Try to fix issue with indent.

luca-heltai · Apr 30, 2023 · 7fc557a · 7fc557a
1 parent 2cbc8fd
commit 7fc557a
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 4 deletions.
diff --git 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
@@ -25,4 +25,5 @@ jobs:
         fetch-depth: 100
     - name: Check indentation
       run: |
+         git config --global --add safe.directory "$GITHUB_WORKSPACE"
          ./scripts/check_indentation.sh 
diff --git 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