Closed ShinKage closed 4 years ago
All the commands failed if the file path contains characters that need to be escaped, such as whitespaces. This patch escapes the path passed as argument to the idris2 command.
Thanks! Does this fix the same thing as #3?
I'm not sure. I have never hit that specific error.
All the commands failed if the file path contains characters that need to be escaped, such as whitespaces. This patch escapes the path passed as argument to the idris2 command.