HEL/midas
1
0
Fork 0
Code Issues Pull Requests Releases Activity

CLI tweaks #22

Merged
HEL merged 3 commits from fix/cli-tweaks into main 2026-06-24 12:18:08 +00:00
Conversation 0 Commits 3 Files Changed 3 +30 -7
HEL commented 2026-06-24 12:18:03 +00:00
Owner
Copy Link

This small PR makes some tweaks to the CLI, including

  • an option for the compile command to ignore errors (--ignore-errors)
  • display of all diagnostics in the types command, not only judgements infos
  • display of diagnostic counts summary by type
This small PR makes some tweaks to the CLI, including - an option for the `compile` command to ignore errors (`--ignore-errors`) - display of all diagnostics in the `types` command, not only judgements infos - display of diagnostic counts summary by type
HEL self-assigned this 2026-06-24 12:18:03 +00:00
HEL added 3 commits 2026-06-24 12:18:03 +00:00
feat(cli): add compile option to ignore errors 6c04e2fee4
fix(cli): show all diagnostics in types command 66f39acec0 
combine type checker diagnostics with judgements info diagnostics
fix(cli): show summary of diagnostic counts 32ed62a6f1
HEL merged commit f7c43837b5 into main 2026-06-24 12:18:08 +00:00
HEL deleted branch fix/cli-tweaks 2026-06-24 12:18:08 +00:00
Sign in to join this conversation.
Reviewers
No Reviewers
Labels
No items
No Label
Milestone
No items
No Milestone
Assignees
Clear assignees
HEL
No Assignees HEL
1 Participants
Notifications
Due Date
No due date set.
Dependencies

No dependencies set.

Reference: HEL/midas#22
Delete Branch "fix/cli-tweaks"

Deleting a branch is permanent. Although the deleted branch may continue to exist for a short time before it actually gets removed, it CANNOT be undone in most cases. Continue?