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 idris2's :cd command requires a quoted string, but the changeDirectory() function does not surround the dir variable with quotes. As a result of this, there are the errors:
I think the compiler is restarted every time any of the compilerOptions change, including the source directory, which makes the invocation of :cd redundant. And currently, I can't reproduce this bug, even though I've hit it before. In fact, I can't tell if that code path is even executed.
The idris2's
:cd
command requires a quoted string, but the changeDirectory() function does not surround thedir
variable with quotes. As a result of this, there are the errors:More than that, if the directory path contains a quote (for example,
/"tmp
), the plugin hangs atIdris: opening REPL ...
.The text was updated successfully, but these errors were encountered: