phc/lean4game
6
1
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

lint: fix line widths

Browse Source
This commit is contained in:
Jon Eugster
2024-01-19 10:50:48 +01:00
parent c103eeacfa
commit fd5e507541
1 changed files with 3 additions and 2 deletions
Download Patch File Download Diff File Expand all files Collapse all files
server/GameServer/FileWorker.lean
+3 -2
View File
@@ -632,8 +632,9 @@ def workerMain (opts : Options) (args : List String): IO UInt32 := do
try try
let some gameDir := args[1]? | throwServerError "Expected second argument: gameDir" let some gameDir := args[1]? | throwServerError "Expected second argument: gameDir"
let exitCode ← initAndRunWorker i o e opts 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 -- HACK: all `Task`s are currently "foreground", i.e. we join on them on main thread exit,
-- want to do that in the case of the worker processes, which can produce non-terminating tasks evaluating user code -- 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 o.flush
e.flush e.flush
IO.Process.exit exitCode.toUInt8 IO.Process.exit exitCode.toUInt8