When Idris returns no proof search, don't delete the metavar

idris-hackers / idris-mode

Idris syntax highlighting, compiler-supported editing, interactive REPL and more things for Emacs.

GNU General Public License v3.0

269 stars 71 forks source link

When Idris returns no proof search, don't delete the metavar #438

Closed david-christiansen closed 6 years ago

david-christiansen commented 7 years ago

Fixes #428.

david-christiansen commented 7 years ago

Looks like the Travis failure is based on a failure of Idris to install properly with its dependencies. When I get time, I'll get the test suite updated to use Stack instead.

abailly commented 6 years ago

Pending #468 and manual testing