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

Fix sysroot issue when running local #139

Closed
wants to merge 1 commit into from

Conversation

eatPizza311
Copy link

Hi,
This PR is addressing #127.
Kindly take a look at the changes, and please let me know if you have any suggestions or need further adjustments.

@gavinleroy
Copy link
Collaborator

gavinleroy commented Sep 30, 2024

Unfortunately, this PR doesn't address #127. the playground isn't launched with the same cargo watch scripts. We're hoping to soon ™️ get rid of the server which would eliminate a whole swath of problems.

Edit, I'm now realizing that the original issue is for the local playground, which this does kind of address. Though setting MIRI_SYSROOT in the server command feels like treating the symptom of the problem and not the issue itself. Getting rid of the server is still what we're trying to do :)

@eatPizza311
Copy link
Author

Yeah, this's an ad hoc fix. I will close this PR, thanks 😉
And thanks for this fantastic tool!

@eatPizza311 eatPizza311 closed this Oct 1, 2024
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.

2 participants