From a7dab88747919980ee89e1c09151a6abba2de7de Mon Sep 17 00:00:00 2001 From: Alexander Bentkamp Date: Tue, 12 Sep 2023 10:14:01 +0200 Subject: [PATCH] remove old debug code --- server/GameServer/FileWorker.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/server/GameServer/FileWorker.lean b/server/GameServer/FileWorker.lean index 979533d..b55adf0 100644 --- a/server/GameServer/FileWorker.lean +++ b/server/GameServer/FileWorker.lean @@ -521,8 +521,6 @@ section MainLoop set st match msg with | Message.request id method (some params) => - -- TODO: What's this error message? - if method == "Game.getInteractiveGoals" then throwServerError "HELLO" handleRequest id method (toJson params) mainLoop | Message.notification "exit" none =>