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

Use hie-bios 0.12 #3524

Merged
merged 2 commits into from
Mar 17, 2023
Merged

Use hie-bios 0.12 #3524

merged 2 commits into from
Mar 17, 2023

Conversation

wz1000
Copy link
Collaborator

@wz1000 wz1000 commented Mar 14, 2023

No description provided.

Copy link
Collaborator

@fendor fendor left a comment

Choose a reason for hiding this comment

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

LGTM. thank you!

@wz1000
Copy link
Collaborator Author

wz1000 commented Mar 15, 2023

@fendor @michaelpj can you please review the logging in Wrappers.hs?

Copy link
Collaborator

@fendor fendor left a comment

Choose a reason for hiding this comment

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

Looks fine as is. However, according to some comments, we can simplify the logging now. Let's get this merged, and then we can look at simplifying the logging story.

You are missing some changes in src/Ide/Main.hs

ghcide/session-loader/Development/IDE/Session.hs Outdated Show resolved Hide resolved
@wz1000 wz1000 force-pushed the wip/hie-bios-0.12 branch 2 times, most recently from 368d849 to 6e8d15e Compare March 15, 2023 13:48
@fendor fendor mentioned this pull request Mar 15, 2023
Copy link
Collaborator

@michaelpj michaelpj left a comment

Choose a reason for hiding this comment

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

Looks fine to me. I think the main knock-on change is that we can now finally purge hslogger.

@wz1000 wz1000 force-pushed the wip/hie-bios-0.12 branch 2 times, most recently from a191a41 to ba4b1cb Compare March 16, 2023 12:53
@wz1000 wz1000 enabled auto-merge (rebase) March 17, 2023 12:17
@wz1000 wz1000 merged commit 385f000 into master Mar 17, 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.

None yet

3 participants