infinite loop = death

[kbuzzard]

In the natural number game, if I go to a world with an a+b in the goal after add_comm is proved (e.g. addition world, level 5) and then I type repeat {rw add_comm} it unsurprisingly goes into an infinite loop. In VS Code one can recover easily by just deleting the repeat line. But in NNG this seems to hang the game completely -- whatever level you go to now, Lean is always busy. Is this an issue with this repo?

Reported by Filip Szczepański on the Lean Zulip chat.

[mpedramfar]

This code is a wrapper around Lean, so I can't see how this issue could be cause by something in this repo. It probably has to do with the browser version of Lean.
In any case, with the new commits, you can simply delete the line and reload the page.