Don't replace newer diagnostics with older ones

2022-11-17 12:21:51 +01:00
parent 532a599239
commit 71eeeedc05
7 changed files with 33 additions and 13 deletions
@@ -652,6 +652,7 @@ message DiagnosticSummary {
    uint64 language_server_id = 2;
    uint32 error_count = 3;
    uint32 warning_count = 4;
+    uint32 version = 5;
 }

 message UpdateLanguageServer {