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

Remove open import syntax #2307

Merged
merged 2 commits into from
Aug 25, 2023
Merged

Remove open import syntax #2307

merged 2 commits into from
Aug 25, 2023

Conversation

lukaszcz
Copy link
Collaborator

@lukaszcz lukaszcz added this to the 0.5 milestone Aug 23, 2023
@lukaszcz lukaszcz self-assigned this Aug 23, 2023
@lukaszcz lukaszcz force-pushed the remove-open-import-syntax branch from 28f2c7b to 4219a48 Compare August 24, 2023 09:42
@lukaszcz lukaszcz marked this pull request as ready for review August 24, 2023 09:43
@lukaszcz lukaszcz requested a review from janmasrovira August 24, 2023 09:43
janmasrovira
janmasrovira previously approved these changes Aug 24, 2023
@janmasrovira janmasrovira dismissed their stale review August 24, 2023 15:33

The merge-base changed after approval.

@lukaszcz lukaszcz force-pushed the remove-open-import-syntax branch from 5ec4f2e to 9da84bd Compare August 24, 2023 15:44
@lukaszcz lukaszcz requested a review from janmasrovira August 25, 2023 08:07
@lukaszcz lukaszcz force-pushed the remove-open-import-syntax branch from 9da84bd to 9c8a57f Compare August 25, 2023 13:29
@janmasrovira janmasrovira merged commit 93a91a7 into main Aug 25, 2023
@janmasrovira janmasrovira deleted the remove-open-import-syntax branch August 25, 2023 14:43
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Drop support for open import syntax
2 participants