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.

Sign up for GitHub

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

Jump to bottom

Agda crashes badly for bad entry in .agda/libraries #1785

Closed
andreasabel opened this issue Jan 19, 2016 · 0 comments
Closed

Agda crashes badly for bad entry in .agda/libraries #1785

andreasabel opened this issue Jan 19, 2016 · 0 comments
Labels
type: bug Issues and pull requests about actual bugs ux: error reporting Issues to do with how Agda reports errors ux: library management Issues relating to the library management system
Milestone
2.5.1

Comments

@andreasabel
Copy link
Member

Just giving a path in .agda/libraries, instead of a filename, like

/home/abel/.agda/

crashes Agda with

/home/abel/.agda/: Failed to read library file
/home/abel/.agda/: openFile: inappropriate type (is a directory)

This should be a proper error message with filename and location, as for other errors.
@andreasabel andreasabel added type: bug Issues and pull requests about actual bugs priority-high ux: error reporting Issues to do with how Agda reports errors ux: library management Issues relating to the library management system labels Jan 19, 2016
@andreasabel andreasabel added this to the 2.4.4 milestone Jan 19, 2016
@andreasabel andreasabel mentioned this issue Jan 26, 2016
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
type: bug Issues and pull requests about actual bugs ux: error reporting Issues to do with how Agda reports errors ux: library management Issues relating to the library management system
Projects
None yet
Milestone
2.5.1
Development

No branches or pull requests
1 participant
@andreasabel