aboutsummaryrefslogtreecommitdiff
path: root/runtime/queries/ocaml-interface
diff options
context:
space:
mode:
authorLuis Useche2024-03-19 11:16:30 +0000
committerGitHub2024-03-19 11:16:30 +0000
commit6a22d7d1cad8fde27d8ba02629c3d33ab535f7b5 (patch)
treefa1748be525a0851eadef48dca8a04333a250d85 /runtime/queries/ocaml-interface
parent4d2282cbccff4dd0aaa901a3ea4fb28a2b8120aa (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/ocaml-interface')
0 files changed, 0 insertions, 0 deletions