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.

Sign up for GitHub

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

Jump to bottom

Provide Access to the Project Name #1759

Merged
merged 7 commits into from
May 27, 2021
Merged

Provide Access to the Project Name #1759

merged 7 commits into from
May 27, 2021

Conversation

iamrecursion
Copy link
Contributor

Pull Request Description

This PR provides facilities needed by the IDE to access the name and properties of the open project.

Closes #1690.

Important Notes

This involves extending the project manager protocol. Assuming that the IDE is robust against new fields in messages this should be fine.

Checklist

Please include the following checklist in your PR:

  • The documentation has been updated if necessary.
  • All code conforms to the Scala, Java, and Rust style guides.
  • All documentation and configuration conforms to the markdown and YAML style guides.
  • All code has been tested where possible.

@iamrecursion iamrecursion added Type: Enhancement --breaking Important: a change that will break a public API or user-facing behaviour p-highest Should be completed ASAP labels May 27, 2021
@iamrecursion iamrecursion requested review from 4e6 and radeusgd May 27, 2021 12:44
@iamrecursion iamrecursion self-assigned this May 27, 2021
@iamrecursion iamrecursion marked this pull request as ready for review May 27, 2021 13:07
@iamrecursion iamrecursion requested a review from kustosz as a code owner May 27, 2021 13:07
4e6
4e6 approved these changes May 27, 2021
View reviewed changes
Copy link
Contributor

@4e6 4e6 left a comment

Choose a reason for hiding this comment

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

Looks good

@iamrecursion iamrecursion merged commit a981e72 into main May 27, 2021
@iamrecursion iamrecursion deleted the wip/ara/project-name branch May 27, 2021 15:13
iamrecursion added a commit that referenced this pull request Jun 24, 2021
@iamrecursion
Provide API access to the project name (#1759)
2ce4036
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@4e6 4e6 4e6 approved these changes

@radeusgd radeusgd Awaiting requested review from radeusgd

@kustosz kustosz Awaiting requested review from kustosz

Assignees

@iamrecursion iamrecursion

Labels
--breaking Important: a change that will break a public API or user-facing behaviour p-highest Should be completed ASAP
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Access to project name
2 participants
@iamrecursion @4e6