editorWidget.border fixed #141
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
|
@arcticicestudio I created a PR with more cosmetic changes which includes this deprecated theme setting: #143 |
svengreb
approved these changes
Jul 20, 2019
arcticicestudio
approved these changes
Jul 20, 2019
There was a problem hiding this comment.
Hi @chris78er 👋, thanks for your contribution 👍
I've tried to reverse the history of this key and if it ever existed in the VS Code code base, but without success. I don't know why the key was ever added like this, maybe I've been too tired 😄
Anyway, thanks for the fix.
arcticicestudio
added
context-ui
scope-compatibility
scope-ux
status-accepted
type-bug
and removed
status-reproduction
labels
|
🚢 Shipped with extension release version 🏷 0.11.0. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Prerequisites
This section and the instructions in the sections below are only part of this pull request template. Please ensure to delete this whole section, all pre-filled instructions of the sections below and sections you have not filled out before submitting to ensure a clear structure and overview.
Please do your best to provide as much information as possible and use a clear and descriptive title for your enhancement suggestion or bug fix to help maintainers and the community understand and reproduce the behavior, find related pull requests and to merge it faster.
developbranch to ensure that the enhancement or bug fix has not already been added.Metadata Head
The metadata head should be added to the top of the pull request as Markdown text quote containing the GitHub issue keyword(s) to link to the related enhancements suggestions (
Closes) or bug reports (Fixes). You can add additional details like dependencies to other pull requests and the order it needs to be merged.Description
Describe the changes as in many relevant details as possible. If this is a enhancement suggestion add specific use-cases and explain why this feature or improvement would be useful. If this is a bug fix ensure to provide a before/after comparison by describing the current behavior and the new behavior.
References
Add any other references and links which are relevant for this pull request.