This repository was archived by the owner on Oct 14, 2023. It is now read-only.
This repository was archived by the owner on Oct 14, 2023. It is now read-only.
leanpkg fails if there's a space in the pathname to the binary #1980
Open
Description
Prerequisites
- [ X] Put an X between the brackets on this line if you have done all of the following:
- Checked that your issue isn't already filed.
- Specifically, check out the wishlist, open RFCs,
or feature requests.
- Specifically, check out the wishlist, open RFCs,
- Reduced the issue to a self-contained, reproducible test case.
- Checked that your issue isn't already filed.
Description
Per title, leanpkg fails if there's a space in the path to the leanpkg executable (OSX, Windows). I know that MSR isn't further developing this version. I'm documenting the issue so that people know and so that it's a known issue. It's causing problems in a large class I'm teaching because many students have spaces in their path names. E.g., many students use Box to store files, and the top-level box directory name has a space in it.
Steps to Reproduce
It's easy to confirm. Just try it.
Expected behavior: leanpkg runs
Actual behavior: leanpkg issues error, main.lean not found
Reproduces how often: reproduces reliably
Versions
3.4.1
Additional Information
Any additional information, configuration or data that might be necessary to reproduce the issue.
Metadata
Metadata
Assignees
Labels
No labels