remove old loop check

3 years ago · bea1790975
parent 15c2f11788
commit bea1790975
1 changed files with 0 additions and 4 deletions
--- 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