wheineman/nrpl

commands which fail to compile should be automatically removed from history to avoid messing up subsequent commands

timotheecour opened this issue · 0 comments

timotheecour commented
commands which fail to compile should be automatically removed from history to avoid messing up subsequent commands