Merge remote-tracking branch 'origin/develop'

runtimeverification · Jun 20, 2024 · f8a9a32 · f8a9a32
2 parents 005fc5c + 24d37d2
commit f8a9a32
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml
@@ -405,6 +405,11 @@ jobs:
           script: |
             const { owner, repo } = context.repo
             await github.rest.repos.updateRelease({ owner, repo, release_id: ${{ needs.set-release-id.outputs.release_id }}, prerelease: false })
+
+  notify-dependents:
+    runs-on: ubuntu-latest
+    needs: release
+    steps:
       - name: 'Update dependents'
         env:
           GITHUB_TOKEN: ${{ secrets.JENKINS_GITHUB_PAT }}