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

GhciEvent: rename to WatcherEvent #338

Merged
merged 1 commit into from
Feb 5, 2025
Merged

GhciEvent: rename to WatcherEvent #338

merged 1 commit into from
Feb 5, 2025

Conversation

lf-
Copy link
Contributor

@lf- lf- commented Feb 4, 2025

This is clearer on its purpose: ghci itself does not generate these events, rather they are events to send to ghci.

  • Labeled the PR with patch, minor, or major to request a version bump when it's merged.
  • Updated the user manual in docs/.
  • Added integration / regression tests in tests/.

This is clearer on its purpose: ghci itself does not generate these
events, rather they are events to send to ghci.
@lf- lf- requested a review from 9999years February 4, 2025 23:51
@github-actions github-actions bot added the patch Bug fixes or non-functional changes label Feb 4, 2025
Copy link
Member

@9999years 9999years left a comment

Choose a reason for hiding this comment

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

reasonable

@lf- lf- merged commit c050796 into main Feb 5, 2025
41 checks passed
@lf- lf- deleted the jade/rename-event branch February 5, 2025 00:15
Copy link
Contributor

github-actions bot commented Feb 5, 2025

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
patch Bug fixes or non-functional changes
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants