Skip to content

[ re #1465 ] Two more modules that are no longer --safe #1498

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

Merged
merged 1 commit into from
May 7, 2021

Conversation

jespercockx
Copy link
Member

It seems there's two modules that slipped through the cracks in #1465 and that should also be made no longer --safe.

@jespercockx jespercockx requested a review from gallais May 6, 2021 14:48
@MatthewDaggitt MatthewDaggitt added safe status: ready upstream Changes induced by Agda upstream labels May 7, 2021
@MatthewDaggitt MatthewDaggitt added this to the agda-v2.6.2 milestone May 7, 2021
@MatthewDaggitt
Copy link
Contributor

Yup I think these were added concurrently to previous pull request 👍

@MatthewDaggitt MatthewDaggitt merged commit e83814b into agda:experimental May 7, 2021
@MatthewDaggitt MatthewDaggitt modified the milestones: agda-v2.6.2, v1.7 May 31, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
safe upstream Changes induced by Agda upstream
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants