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
(Found at 6fc713d, consistent at least back through 0.9.18)
Bogus command line arguments given to idris --client print a usage message (good!) and then exit with status 0 (less good). This means that programs calling out to idris don't realize their command lines are formatted incorrectly.
I specifically noticed this with the idris-vim plugin, resulting in the issue idris-hackers/idris-vim#39.
Test case (note that idris requires quotes around the :l file.idr command):
(Found at 6fc713d, consistent at least back through 0.9.18)
Bogus command line arguments given to
idris --client
print a usage message (good!) and then exit with status 0 (less good). This means that programs calling out toidris
don't realize their command lines are formatted incorrectly.I specifically noticed this with the idris-vim plugin, resulting in the issue idris-hackers/idris-vim#39.
Test case (note that
idris
requires quotes around the:l file.idr
command):The text was updated successfully, but these errors were encountered: