projects / cvc5.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: 078759e)
Also run on created. (#8506)
authorGereon Kremer <gkremer@cs.stanford.edu>
Fri, 1 Apr 2022 00:44:49 +0000 (02:44 +0200)
committerGitHub <noreply@github.com>
Fri, 1 Apr 2022 00:44:49 +0000 (17:44 -0700)
The way we now create releases apparently does not trigger the release::published event. It should trigger the release::created event, though.

.github/workflows/package_pypi.yml patch | blob | history

diff --git a/.github/workflows/package_pypi.yml b/.github/workflows/package_pypi.yml
index 53e0d3d3db705685da1b6e762df47ebf42fa41cd..79c740157b922b6c8b5c6f67e6d523f20f8fc7ba 100644 (file)
--- a/.github/workflows/package_pypi.yml
+++ b/.github/workflows/package_pypi.yml
@@ -1,6 +1,6 @@
 on:
   release:
-    types: [published]
+    types: [created, published]
   schedule:
     - cron: '0 1 * * *'