diff options
author | bors[bot] <26634292+bors[bot]@users.noreply.github.com> | 2020-05-04 04:03:52 +0100 |
---|---|---|
committer | GitHub <[email protected]> | 2020-05-04 04:03:52 +0100 |
commit | 57ec813294368a25e424672ad13bcee47f19f1d2 (patch) | |
tree | 7ea4b38e450a3f6f1f81b3f7f6fa80d570b63c3b /crates/ra_hir_def/src/keys.rs | |
parent | 805c0b92ac577dcb8c4cddf567a2c7e216c4259c (diff) | |
parent | 87a18b18eab859cbfcbaf178bc6355215dae8381 (diff) |
Merge #4286
4286: Make incremental sync opt-in r=matklad a=lnicola
@matklad do you want to merge this? I'd make it opt-out, but it's fine to test it more.
Co-authored-by: Laurențiu Nicola <[email protected]>
Diffstat (limited to 'crates/ra_hir_def/src/keys.rs')
0 files changed, 0 insertions, 0 deletions