You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
The idris-vim Syntastic integration is generating command lines of the form
idris --client :l filename.idr
which causes Idris to bomb out with a usage message. (Unfortunately it returns 0 when it does so, so vim provides no indication that something's wrong.)
The command line needs to be of the form
idris --client ":l filename.idr"
because Idris appears to be processing individual argument strings as commands, not the entire set of arguments.
I've managed to fake this in the current version by abusing args and post_args to surround the command with quotes. This works only because Idris is tolerant of whitespace before and after filenames; it isn't clear how it would work with a filename e.g. containing whitespace.
The text was updated successfully, but these errors were encountered:
(idris-vim commit 45680a3, Idris 0.9.19.)
The idris-vim Syntastic integration is generating command lines of the form
which causes Idris to bomb out with a usage message. (Unfortunately it returns 0 when it does so, so vim provides no indication that something's wrong.)
The command line needs to be of the form
because Idris appears to be processing individual argument strings as commands, not the entire set of arguments.
I've managed to fake this in the current version by abusing
args
andpost_args
to surround the command with quotes. This works only because Idris is tolerant of whitespace before and after filenames; it isn't clear how it would work with a filename e.g. containing whitespace.The text was updated successfully, but these errors were encountered: