diff options
author | bors[bot] <26634292+bors[bot]@users.noreply.github.com> | 2021-01-07 14:39:50 +0000 |
---|---|---|
committer | GitHub <[email protected]> | 2021-01-07 14:39:50 +0000 |
commit | aa9bef07971493e3edd8f9179d05920cbfc8160b (patch) | |
tree | 6df3bba47d9184f4fffea7497e29298196150a15 /.github/workflows/release.yaml | |
parent | 7967ce85cfc5fc2b1996425b44f2a45d0841c8ff (diff) | |
parent | c547ec1cd6fb764d7ad7c1e8b066b90038b44920 (diff) |
Merge #7194
7194: Don't update the server if managed by the user r=matklad a=lnicola
Fixes #7187
CC @figsoda
Co-authored-by: Laurențiu Nicola <[email protected]>
Diffstat (limited to '.github/workflows/release.yaml')
0 files changed, 0 insertions, 0 deletions