Rename GPG public key in releases #1294

jpraynaud · 2023-10-13T09:26:17Z

Content

This PR includes the renaming of the GPG public key in the releases from gpg-public.key to public-key.gpg

Branch
- Commit sequence broadly makes sense
- Key commits have useful messages
PR
- No clippy warnings in the CI
- Self-reviewed the diff
- Useful pull request description
- Reviewer requested

Closes #1292

github-actions · 2023-10-13T09:39:54Z

    3 files ±0   17 suites ±0 6m 31s ⏱️ +49s
699 tests ±0 699 ✔️ ±0 0 💤 ±0 0 ❌ ±0
757 runs ±0 757 ✔️ ±0 0 💤 ±0 0 ❌ ±0

Results for commit 358788e. ± Comparison against base commit 75dfb67.

Rename GPG public key in releases

358788e

jpraynaud self-assigned this Oct 13, 2023

jpraynaud requested review from ghubertpalo and dlachaume October 13, 2023 09:26

dlachaume approved these changes Oct 13, 2023

View reviewed changes

jpraynaud temporarily deployed to testing-preview October 13, 2023 09:45 — with GitHub Actions Inactive

jpraynaud requested a review from Alenar October 13, 2023 13:35

ghubertpalo approved these changes Oct 16, 2023

View reviewed changes

jpraynaud merged commit 5d3de6d into main Oct 16, 2023

jpraynaud deleted the jpraynaud/1292-rename-gpg-public-key-release branch October 16, 2023 07:35