Skip to content

Make model editor top banner sticky#3120

Merged
norascheuch merged 4 commits intomainfrom
nora/make-top-banner-sticky
Dec 8, 2023
Merged

Make model editor top banner sticky#3120
norascheuch merged 4 commits intomainfrom
nora/make-top-banner-sticky

Conversation

@norascheuch
Copy link
Copy Markdown
Contributor

@norascheuch norascheuch commented Dec 8, 2023

Before:
Screenshot 2023-12-08 at 15 07 44

After:
https://github.com/github/vscode-codeql/assets/29482385/a6d6aff3-8a86-4cd6-bc57-cbb8101d379f

Checklist

  • CHANGELOG.md has been updated to incorporate all user visible changes made by this pull request.
  • Issues have been created for any UI or other user-facing changes made by this pull request.
  • [Maintainers only] If this pull request makes user-facing changes that require documentation changes, open a corresponding docs pull request in the github/codeql repo and add the ready-for-doc-review label there.

@norascheuch norascheuch marked this pull request as ready for review December 8, 2023 14:14
@norascheuch norascheuch requested review from a team as code owners December 8, 2023 14:14
display: flex;
flex-direction: row;
align-items: end;
background-color: var(--vscode-editorGutter-background);
Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

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

Is there a specific reason why this is editorGutter-background rather than editor-background? Usually these two colors match, but if we want to match the background color of the webview, we should use editor-background.

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

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

Oh, just a mistake when copying the variable. Updated it!

@norascheuch norascheuch enabled auto-merge December 8, 2023 15:10
@norascheuch norascheuch merged commit 4f85ac1 into main Dec 8, 2023
@norascheuch norascheuch deleted the nora/make-top-banner-sticky branch December 8, 2023 15:24
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