Merge branch 'main' into isofibrations

emilyriehl · Nov 9, 2024 · 186a133 · 186a133
2 parents ae4c359 + 26ebe71
commit 186a133
Show file tree

Hide file tree

Showing 2 changed files with 14 additions and 0 deletions.
diff --git a/.github/workflows/blueprint.yml b/.github/workflows/blueprint.yml
@@ -145,3 +145,15 @@ jobs:
         if: github.event_name == 'push'
         id: deployment
         uses: actions/deploy-pages@v4
+
+  # Enable status check to ensure all jobs succeeded
+  check:
+    if: always()
+    needs:
+    - build_project
+    runs-on: Ubuntu-latest
+    steps:
+    - name: Decide whether the needed jobs succeeded or failed
+      uses: re-actors/alls-green@release/v1
+      with:
+        jobs: ${{ toJSON(needs) }}
diff --git a/.github/workflows/create-release.yml b/.github/workflows/create-release.yml
@@ -4,6 +4,8 @@ on:
   push:
     branches:
       - main
+    paths:
+      - 'lean-toolchain'
 
 jobs:
   create-release:
-Original file line number
+Diff line change
@@ Expand Up / @@ -4,6 +4,8 @@ on: @@
       push:
         branches:
           - main
+        paths:
+          - 'lean-toolchain'
     jobs:
       create-release:
@@ Expand Down @@