Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Allow ipkg sourcedir to have deep location #4619

Merged
merged 2 commits into from
Dec 20, 2018

Conversation

shmish111
Copy link

Copy link
Contributor

@melted melted left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This requires the dir to be quoted. Breaking compatibility and it’s not so nice in a config file. Either we should allow both forms (easy to do), or we should parse an unquoted path (harder).

@melted
Copy link
Contributor

melted commented Dec 17, 2018

Hmmm. Can we just read to the newline, trim whitespace and parse that as a path?

Thanks for the PR anyway!

@shmish111
Copy link
Author

Good point @melted so I've implemented the easy option in this new commit. I find it quite normal to allow simple things unquoted and complicated things quoted.

@shmish111
Copy link
Author

What tends to be the release schedule for Idris? Not being pushy here, just want to get some idea of how long bugs like this tend to get fixed. Also @melted is my PR ok now that I have enabled quoted and unquoted parsing?

@melted
Copy link
Contributor

melted commented Dec 20, 2018

@shmish111 Work on Idris has slowed down (with all the effort Edwin is putting into Blodwen, Idris in Idris), but there have been several releases a year even so. But the exact timing depends on need, a new release of GHC usually provides motivation with breaking code.

@melted melted merged commit 7855f86 into idris-lang:master Dec 20, 2018
@shmish111
Copy link
Author

That's awesome thanks @melted

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants