From e61799a77fffb3afb37af3dd3cbae87785a8f18f Mon Sep 17 00:00:00 2001 From: Mariana Alanis Date: Tue, 14 Jun 2022 15:31:08 -0500 Subject: [PATCH] fix: add a better handling in case only worker crashes (CR comments) --- src/Lean/Server/Watchdog.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean index 1b0ae8c662..d35a7a778a 100644 --- a/src/Lean/Server/Watchdog.lean +++ b/src/Lean/Server/Watchdog.lean @@ -259,7 +259,7 @@ section ServerM else -- Worker crashed fw.errorPendingRequests o (if exitCode = 1 then ErrorCode.workerCrashed else ErrorCode.stackOverflow) - s!"Server process for {fw.doc.meta.uri} crashed, {if exitCode = 1 then "see stderr for exception" else "likely due to a stack overflow or a bug in "user's" code"}." + s!"Server process for {fw.doc.meta.uri} crashed, {if exitCode = 1 then "see stderr for exception" else "likely due to a stack overflow or a bug in user code"}." return WorkerEvent.crashed err loop let task ← IO.asTask (loop $ ←read) Task.Priority.dedicated