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.

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

idris2 --init doesn't check a name of a package #3232

Open
DanMax03 opened this issue Mar 9, 2024 · 0 comments
Open

idris2 --init doesn't check a name of a package #3232

DanMax03 opened this issue Mar 9, 2024 · 0 comments
Labels
cli: package init status: confirmed bug Something isn't working

Comments

@DanMax03
Copy link

DanMax03 commented Mar 9, 2024

Steps to Reproduce

  1. Call idris2 --init
  2. Give a name for a package that is not a correct Idris identificator, i.e. 123_Issue
  3. Finish the package in any reasonable way (at least set everything else empty)

Expected Behavior

The program doesn't allow such a name for a package since it doesn't compile

Observed Behavior

The program allows to create a package with such a name
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
cli: package init status: confirmed bug Something isn't working
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@gallais @DanMax03