Skip to content

Commit

Permalink
Attempt to fix the stability of DocumentAddedToExistingProjectDoesNot…
Browse files Browse the repository at this point in the history
…Crash (#5456)

Fixes #5434

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
  • Loading branch information
keyboardDrummer committed May 17, 2024
1 parent 55ab7fd commit 80583b7
Showing 1 changed file with 1 addition and 0 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -373,6 +373,7 @@ import Library
// Change in file1 causes project detection to realize it's now part of project, so it is added there.
ApplyChange(ref file1, new Range(0, 0, 0, 0), "// added this comment\n");
ApplyChange(ref file2, new Range(0, 0, 0, 0), "// added this comment\n");
await client.WaitForNotificationCompletionAsync(project.Uri, CancellationToken);
var diagnostics0 = await GetLastDiagnostics(project);
var diagnostics1 = await GetLastDiagnostics(file1);
var diagnostics2 = await GetLastDiagnostics(file2);
Expand Down

0 comments on commit 80583b7

Please sign in to comment.