Skip to content

Commit b822368

Browse files
committed
Enable redoing upload release CI (#2275)
Without having to push a new release
1 parent cec6a18 commit b822368

File tree

1 file changed

+8
-1
lines changed

1 file changed

+8
-1
lines changed

.github/workflows/release.yml

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -213,7 +213,14 @@ jobs:
213213
214214
- name: Release
215215
run: |
216-
gh release create $TAG_NAME $PRERELEASE --notes-file "$RUNNER_TEMP/notes.md" --title "$SUBJECT" --target $GITHUB_SHA flint-${FLINT_VERSION}.{tar.gz,tar.xz,zip}
216+
# In the case that some thing after the release failed, we still want
217+
# to be able to rerun it without having to create a new release.
218+
API_URL="https://api.github.com/repos/flintlib/flint/releases/tags/v${FLINT_VERSION}"
219+
response=$(curl -s -o /dev/null -w "%{http_code}" "$API_URL")
220+
if test "$response" != "200";
221+
then
222+
gh release create $TAG_NAME $PRERELEASE --notes-file "$RUNNER_TEMP/notes.md" --title "$SUBJECT" --target $GITHUB_SHA flint-${FLINT_VERSION}.{tar.gz,tar.xz,zip}
223+
fi
217224
218225
- if: env.TAG_NAME != 'nightly'
219226
name: "Build PDF documentation"

0 commit comments

Comments
 (0)