From 04cda4357f6e062c1c4ec95217726706d4034590 Mon Sep 17 00:00:00 2001 From: Rob Lourens Date: Mon, 25 Jun 2018 13:32:57 -0700 Subject: [PATCH] #52810 - Tweak settings editor header padding --- .../parts/preferences/browser/media/settingsEditor2.css | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/vs/workbench/parts/preferences/browser/media/settingsEditor2.css b/src/vs/workbench/parts/preferences/browser/media/settingsEditor2.css index 031fe1744d5..2e65d0448ab 100644 --- a/src/vs/workbench/parts/preferences/browser/media/settingsEditor2.css +++ b/src/vs/workbench/parts/preferences/browser/media/settingsEditor2.css @@ -35,7 +35,7 @@ .settings-editor > .settings-header > .settings-advanced-customization { opacity: .7; - margin-top: 10px; + margin-top: 8px; } .settings-editor > .settings-header > .settings-preview-header > .settings-preview-warning { @@ -67,7 +67,7 @@ } .settings-editor > .settings-header > .settings-header-controls { - margin-top: 2px; + margin-top: 3px; height: 30px; display: flex; } -- GitLab