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

The Idris Errors panel should tell me if typechecking went successfully #43

Closed
NightRa opened this issue Aug 8, 2015 · 2 comments
Closed
Milestone

Comments

@NightRa
Copy link
Contributor

NightRa commented Aug 8, 2015

If I do typecheck and it fails, it raises the Idris Errors panel.
If I fix everything, typecheck again and it succeeds, currently there is no response what-so-ever and the old type error is still present.
I think there should be some indication that typechecking succeeded, and the old type error should not be displayed anymore.

@archaeron
Copy link
Member

hello
there is a PR for this. :)
#40

need to check something and then I can merge it

expect this in the next version

@archaeron archaeron added this to the 0.3.0 milestone Aug 8, 2015
@archaeron archaeron modified the milestones: 0.2.5, 0.3.0 Aug 8, 2015
@archaeron
Copy link
Member

this is now in master and is ready for the next version
d2b6a86

thanks to @edwinb for this

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

No branches or pull requests

2 participants