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

enableInitializersExecution

Browse Source
This commit is contained in:
Alexander Bentkamp
2022-12-05 16:25:20 +01:00
parent 0a495984aa
commit eda5357723
1 changed files with 4 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files
server/leanserver/Main.lean
+4 -1
View File
@@ -2,8 +2,11 @@ import GameServer.Watchdog
import GameServer.FileWorker import GameServer.FileWorker
def main : List String → IO UInt32 := fun args => do unsafe def main : List String → IO UInt32 := fun args => do
let e ← IO.getStderr let e ← IO.getStderr
Lean.enableInitializersExecution
if args[0]? == some "--server" then if args[0]? == some "--server" then
MyServer.Watchdog.watchdogMain [] MyServer.Watchdog.watchdogMain []
else if args[0]? == some "--worker" then else if args[0]? == some "--worker" then