You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Take a file that takes idris2 a while to type-check, say Foo.idr.
While idris2 is type-checking, make a change in the file and save before idris2 finishes.
Reload the file.
Expected Behavior
Main> :r
1/1 Building Main (Foo.idr)
Main>
Observed Behavior
Main> :r
Main>
I think this is because the timestamp on the last change to this file is taken after type-checking finishes, and it should be taken before type-checking starts.
The text was updated successfully, but these errors were encountered:
melted
pushed a commit
to melted/Idris2
that referenced
this issue
Jun 1, 2020
Issue by ohad
Friday Oct 18, 2019 at 12:17 GMT
Originally opened as edwinb/Idris2-boot#127
Steps to Reproduce
Take a file that takes idris2 a while to type-check, say
Foo.idr
.While idris2 is type-checking, make a change in the file and save before idris2 finishes.
Reload the file.
Expected Behavior
Observed Behavior
I think this is because the timestamp on the last change to this file is taken after type-checking finishes, and it should be taken before type-checking starts.
The text was updated successfully, but these errors were encountered: