lean4-htt/.github
Joachim Breitner 7283e2c14e
chore: pr-release: pass --retry to curl (#5025)
Since https://github.com/curl/curl/pull/4465 curl adheres to the
`Retry-After` header, so maybe this fixes the issues with
```
jq: error (at <stdin>:5): Cannot index string with string "body"
```
that sometimes make this workflow fail.
2024-08-13 16:19:43 +00:00
..
ISSUE_TEMPLATE chore: bug template: point to live.lean-lang.org (#4109) 2024-05-08 13:21:17 +00:00
workflows chore: pr-release: pass --retry to curl (#5025) 2024-08-13 16:19:43 +00:00
PULL_REQUEST_TEMPLATE.md chore: refine PR template (#3074) 2023-12-18 13:47:04 +00:00