8000 Fixed #7199 by nad · Pull Request #7454 · agda/agda · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Fixed #7199 #7454

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
Merged
merged 1 commit into from
Aug 29, 2024
Merged

Fixed #7199 #7454

merged 1 commit into from
Aug 29, 2024

Conversation

nad
Copy link
Contributor
@nad nad commented Aug 26, 2024 •
edited by andreasabel
Loading

@nad nad added this to the 2.7.0.1 milestone Aug 26, 2024
@nad nad self-assigned this Aug 26, 2024
@nad nad requested a review from andreasabel August 26, 2024 20:42
andreasabel
andreasabel reviewed Aug 27, 2024
View reviewed changes
Copy link
Member
@andreasabel andreasabel left a comment

Choose a reason for hiding this comment

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

@nad Can you summarise in a few words what this patch does?

@nad
Copy link
Contributor Author
nad commented Aug 27, 2024

I tried to change the code so that, if the cached hash does not match the hash in the interface file, then the interface file is reloaded.

andreasabel
andreasabel approved these changes Aug 28, 2024
View reviewed changes
Copy link
Member
@andreasabel andreasabel left a comment

Choose a reason for hiding this comment

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

Thanks!

@andreasabel andreasabel added the interface Serialization and loading of interface files label Aug 28, 2024
@andreasabel
Copy link
Member

@nad Please merge when you are ready!

@nad nad merged commit fde357c into master Aug 29, 2024
28 checks passed
@nad nad deleted the issue7199 branch August 29, 2024 18:04
@andreasabel
Copy link
Member

Cherry-picked onto

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@andreasabel andreasabel andreasabel approved these changes

Assignees

@nad nad

Labels
interface Serialization and loading of interface files
Projects
None yet
Milestone
2.7.0.1
Development

Successfully merging this pull request may close these issues.

Agda re-checks a file with an up-to-date interface file
2 participants
@nad @andreasabel
0