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

Disallow user from importing several Arend modules at once. #409

Closed
sxhya opened this issue Jul 25, 2023 · 1 comment
Closed

Disallow user from importing several Arend modules at once. #409

sxhya opened this issue Jul 25, 2023 · 1 comment
Assignees

Comments

@sxhya
Copy link
Collaborator

sxhya commented Jul 25, 2023

In the attached gif you can see that importing a directory with 2 Arend modules is allowed and that no errors are reported.

Peek 2023-07-25 12-15

I propose to do the following.

Import Arend module feature should recursively scan for arend.yaml files in the folder tree. If no YAML-files are found, warning should be given to the user. If multiple YAML files are found, 1 Arend module should be created per each Yaml. The situation mentioned in the video should not happen.

@valis
Copy link
Collaborator

valis commented Aug 24, 2023

There should be just 1 yaml file in the root. No scanning is required.

alex999990009 pushed a commit to alex999990009/intellij-arend that referenced this issue Oct 18, 2023
@sxhya sxhya closed this as completed in a597be8 Oct 25, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

3 participants