MichelNielsen (7) [Avatar] Offline
#1
Today I was playing with some code example in vim with the idris plugin and happily doing some automatic refinements and stuff...
However, after a while I discovered that some code was gone. I suspect that the code vanished because I was running a program (:exec replWith .....) in the idris REPL while doing refinements, checking types and docs and so on from within vim.

The problem might only exist when using vim, however I felt that I better post a warning to prevent other poor souls from suddenly loosing a lot of code..
It was just a few lines in my case (undo not possible since I had many edits I didn't want to loose), but I can imagine scary scenarios with hours of work lost.