-
Notifications
You must be signed in to change notification settings - Fork 1.3k
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
Rename editor preference section heading #7428
Conversation
[APPROVALNOTIFIER] This PR is NOT APPROVED This pull-request has been approved by: Associated issue: #6602 The full list of commands accepted by this bot can be found here.
Needs approval from an approver in each of these files:
Approvers can indicate their approval by writing |
@jeanp413 what do you think of this change? Took a bias for action and opened this. Feel free to also close if it does not look like a good MVC (minimum viable change) or pick this up if there's more to change. Cc @akosyakov @loujaybee |
/werft run 👍 started the job as gitpod-build-gt-rename-editor-preference-section-title.2 |
6e8a3b4
to
15a2e26
Compare
/werft run with-clean-slate-deployment 👍 started the job as gitpod-build-gt-rename-editor-preference-section-title.4 |
/werft run with-helm 👍 started the job as gitpod-build-gt-rename-editor-preference-section-title.5 |
Changes look fine for me but not sure why the build is failing |
/werft run with-clean-slate-deployment with-helm 👍 started the job as gitpod-build-gt-rename-editor-preference-section-title.6 |
/werft run with-clean-slate-deployment 👍 started the job as gitpod-build-gt-rename-editor-preference-section-title.7 |
ah I see the branch name is too long. @gtsiolis I think you need to create another PR with a shorter name
|
Description
This will update the IDE (Editor) preference section heading from Default IDE to Editor.
This can probably be further improved in #6602.
See relevant discussion (internal).
How to test
Go to
/preferences
.Release Notes