edwinb / Idris2-boot

A dependently typed programming language, a successor to Idris
https://idris-lang.org/
Other
902 stars 58 forks source link

Allow spaces in file path for generated Chez programs #299

Closed chrrasmussen closed 4 years ago

chrrasmussen commented 4 years ago

If one try to execute an Idris 2 program (idris2 --exec main Main.idr) where Main.idr is located in a folder with spaces, the generated Chez program will fail to run. Instead it shows an error message like:

build/exec/_tmpchez: line 4: /Users/username/Library/Mobile: No such file or directory

I added a test where idris2 is run inside a folder with spaces. (I named the test chez016 because chez015 is already taken by #284)

This issue was originally introduced in fd7a2e5.

edwinb commented 4 years ago

Thanks for the fix. Something funny has happened with the test numbering though - would you mind updating it, then I'll merge? Ta.

chrrasmussen commented 4 years ago

Interestingly, I could resolve the conflict directly from the GitHub page. It is now ready to be merged :)

edwinb commented 4 years ago

Splendid, thank you!