[ ci ] ignore Release/ for idris2 builds

gallais · gallais · commit 0e4168edbf9e · 2021-08-31T13:56:45.000+01:00
diff --git a/.github/workflows/ci-idris2.yml b/.github/workflows/ci-idris2.yml
@@ -9,6 +9,7 @@ on:
     paths-ignore:
       - 'docs/**'
       - 'icons/**'
+      - 'Release/**'
       - '*.md'
       - 'CONTRIBUTORS'
       - 'LICENSE'
