From fd5e50754104d307b098b461da2a76fcdb70f0dd Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Fri, 19 Jan 2024 10:50:48 +0100 Subject: [PATCH] lint: fix line widths --- server/GameServer/FileWorker.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/server/GameServer/FileWorker.lean b/server/GameServer/FileWorker.lean index aa1d80a..6ca86c3 100644 --- a/server/GameServer/FileWorker.lean +++ b/server/GameServer/FileWorker.lean @@ -632,8 +632,9 @@ def workerMain (opts : Options) (args : List String): IO UInt32 := do try let some gameDir := args[1]? | throwServerError "Expected second argument: gameDir" let exitCode ← initAndRunWorker i o e opts gameDir - -- HACK: all `Task`s are currently "foreground", i.e. we join on them on main thread exit, but we definitely don't - -- want to do that in the case of the worker processes, which can produce non-terminating tasks evaluating user code + -- HACK: all `Task`s are currently "foreground", i.e. we join on them on main thread exit, + -- but we definitely don't want to do that in the case of the worker processes, + -- which can produce non-terminating tasks evaluating user code. o.flush e.flush IO.Process.exit exitCode.toUInt8