search

leanprover-community / lean4game

Server to host lean games.
https://adam.math.hhu.de
GNU General Public License v3.0
199 stars 35 forks source link

Commandline looses proof history #85

Closed joneugster closed 1 year ago

joneugster commented 1 year ago

Reproduction:

  1. open a level, enter a tactic.
  2. got one level back, one forward.
  3. enter a new tactic
  4. the first tactic is lost :(
joneugster commented 1 year ago

Fixed by other changes / not reproducible anymore.