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

Add extra help line for delete command #4302

Merged
merged 4 commits into from
Sep 5, 2023
Merged

Add extra help line for delete command #4302

merged 4 commits into from
Sep 5, 2023

Conversation

sixfourtwelve
Copy link
Contributor

@sixfourtwelve sixfourtwelve commented Sep 5, 2023

Overview

Provides one extra help info for the delete command

Before:

.> help delete

  delete
  `delete foo` removes the term or type name `foo` from the namespace.

After:

.> help delete

  delete
  `delete foo` removes the term or type name `foo` from the namespace.
  `delete foo bar` removes the term or type name `foo` and `bar` from the namespace

Implementation notes

How does it accomplish it, in broad strokes? i.e. How does it change the Haskell codebase?

Test coverage

Manual testing

@sixfourtwelve sixfourtwelve changed the title Add extra help line for delete command Add extra help line for delete command (https://github.com/unisonweb/unison/issues/4194) Sep 5, 2023
@sixfourtwelve sixfourtwelve changed the title Add extra help line for delete command (https://github.com/unisonweb/unison/issues/4194) Add extra help line for delete command Sep 5, 2023
@sixfourtwelve
Copy link
Contributor Author

Fixes #4194

Copy link
Contributor

@ceedubs ceedubs left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thank you! 🎉

@aryairani aryairani added the ready-to-merge Apply this to a PR and it will get merged automatically once CI passes and 1 reviewer has approved label Sep 5, 2023
@mergify mergify bot merged commit 00531f6 into unisonweb:trunk Sep 5, 2023
6 checks passed
@mergify mergify bot removed the ready-to-merge Apply this to a PR and it will get merged automatically once CI passes and 1 reviewer has approved label Sep 5, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants