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 /crates/arena/src/lib.rs | |
| 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 'crates/arena/src/lib.rs')
0 files changed, 0 insertions, 0 deletions