diff options
| author | Luis Useche | 2024-03-19 11:16:30 +0000 |
|---|---|---|
| committer | GitHub | 2024-03-19 11:16:30 +0000 |
| commit | 6a22d7d1cad8fde27d8ba02629c3d33ab535f7b5 (patch) | |
| tree | fa1748be525a0851eadef48dca8a04333a250d85 /runtime/queries/unison | |
| parent | 4d2282cbccff4dd0aaa901a3ea4fb28a2b8120aa (diff) | |
Do not stop reloading docs on error (#9870)
In the `reload-all` command, we should not stop reloading the documents
if one error is found. Instead, we should report the error and continue
trying to reload the current open documents. This is useful in cases
where a backing file does not exist temporarily (e.g. when editing a git
patch in the outstanding chain that doesn't have a file just yet).
This change also remove the error messages in the cases where the
backing is `None`, like in new docs or `tutor`.
Diffstat (limited to 'runtime/queries/unison')
0 files changed, 0 insertions, 0 deletions