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

Fix check for module name for Orphan Juvix files and imports of Juvix Markdown files #2512

Merged
merged 11 commits into from
Nov 17, 2023

Conversation

jonaprieto
Copy link
Collaborator

@jonaprieto jonaprieto commented Nov 10, 2023

@jonaprieto jonaprieto added the enhancement New feature or request label Nov 17, 2023
@jonaprieto jonaprieto marked this pull request as ready for review November 17, 2023 10:32
@jonaprieto jonaprieto merged commit dd43f07 into main Nov 17, 2023
4 checks passed
@jonaprieto jonaprieto deleted the fix-wrong-top-modulename branch November 17, 2023 15:10
@jonaprieto jonaprieto changed the title Fix #2510 Fix Check module name for Orphan Juvix files and imports of Juvix Markdown files Nov 17, 2023
@jonaprieto jonaprieto changed the title Fix Check module name for Orphan Juvix files and imports of Juvix Markdown files Fix check for module name for Orphan Juvix files and imports of Juvix Markdown files Nov 17, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request fix:bug
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Error importing module declared in .juvix.md file Orphan Juvix files can have any module name
2 participants