From bea17909751eced66397d2b2ca45677821952fd5 Mon Sep 17 00:00:00 2001
From: Alexander Bentkamp <bentkamp@gmail.com>
Date: Tue, 11 Jul 2023 13:47:02 +0200
Subject: [PATCH] remove old loop check

---
 server/GameServer/Commands.lean | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/server/GameServer/Commands.lean b/server/GameServer/Commands.lean
index 23c8edb..e2dc042 100644
--- a/server/GameServer/Commands.lean
+++ b/server/GameServer/Commands.lean
@@ -678,10 +678,6 @@ tactics are available in each level etc. -/
 elab "MakeGame" : command => do
   let game ← getCurGame
 
-  -- Check for loops in world graph
-  if game.worlds.hasLoops then
-    throwError "World graph must not contain loops! Check your `Path` declarations."
-
   let env ← getEnv
 
   -- Now create The doc entries from the templates