diff options
| author | bors[bot] <bors[bot]@users.noreply.github.com> | 2019-04-17 06:51:12 +0100 |
|---|---|---|
| committer | bors[bot] <bors[bot]@users.noreply.github.com> | 2019-04-17 06:51:12 +0100 |
| commit | d3afb1b3782683c3e800b38b4c24b7581918fb7f (patch) | |
| tree | d9a37343c1227c94eaefc54671ddb562faeaf20c /crates/tools/src/main.rs | |
| parent | 0e35603069b4f3cee97641204b09d91fd723d01d (diff) | |
| parent | 8d569d49d2508cd7b50dd3d00d5509d4128bf645 (diff) | |
Merge #1153
1153: "Restart server" command r=jrvidal a=jrvidal
The only tricky aspect is that fact that once the `exit` command has been received, we no longer need to join on the reader thread.
Also, I think `terminateProcesses.sh` was not working properly. In fact, the very same script from the vscode language server implementation is not working either! It's because of that I noticed the reader thread issue :open_mouth:
Co-authored-by: Roberto Vidal <[email protected]>
Diffstat (limited to 'crates/tools/src/main.rs')
0 files changed, 0 insertions, 0 deletions