idris-hackers / idris-vim

Idris mode for vim
221 stars 52 forks source link

Documentation issue with <LeaderKey> instead of "\" #91

Open stephane-rolland opened 5 years ago

stephane-rolland commented 5 years ago

It took me a long time to find out why I thought vim-idris was not working although the plugin was loaded:

As a consequence none of the commands in the documentation were working.

So I tend to think you should modify the documentation and replace LeaderKey by back-slash \

vkorenev commented 4 years ago

Documentation mentions <LocalLeader>, which is different from <leader> although both of them are mapped to backslash by default.