diff options
| author | Laurențiu Nicola <[email protected]> | 2020-09-18 20:15:44 +0100 |
|---|---|---|
| committer | Laurențiu Nicola <[email protected]> | 2020-09-18 20:15:44 +0100 |
| commit | 5a0bad77543f9bf6df84e6c96b903683f8d23a5e (patch) | |
| tree | 2e69edfa37d63364ca74d909d1288f1354b79cfe /docs/dev | |
| parent | c217bc561f6458f8f9f1133e25635ba32e71e7db (diff) | |
Don't re-read open files from disk when reloading a workspace
Diffstat (limited to 'docs/dev')
0 files changed, 0 insertions, 0 deletions