Make reconnects smoother for dev servers (#12223)

Release Notes: - N/A Co-authored-by: Nathan <nathan@zed.dev>
2024-05-23 21:11:14 -06:00
parent 656edc4b2e
commit 3ec94697b4
3 changed files with 28 additions and 9 deletions
@@ -510,6 +510,7 @@ message CreateDevServerResponse {
 }

 message ShutdownDevServer {
+    optional string reason = 1;
 }

 message RenameDevServer {