From 3a99fe5d65f683e1c63fe41fc888ff9d2abf71ad Mon Sep 17 00:00:00 2001 From: Johann Hubert Sonntagbauer Date: Tue, 1 May 2018 14:41:25 +0200 Subject: [PATCH] [playground] fix overflow in safari (#4406) * [playground] fix overflow in safari * options panel will not outgrow editors panel * fix overflow in safari 10.1 * fix odd code mirror gutter placement during overflow --- website/static/separate-css/playground.css | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/website/static/separate-css/playground.css b/website/static/separate-css/playground.css index 536d8c062..009c041a2 100644 --- a/website/static/separate-css/playground.css +++ b/website/static/separate-css/playground.css @@ -145,6 +145,10 @@ pre.CodeMirror-placeholder { color: #888888; } +.editors .CodeMirror-scroll { + position: static; +} + .bottom-bar { position: relative; } @@ -180,7 +184,7 @@ pre.CodeMirror-placeholder { display: none; box-sizing: border-box; width: 225px; - height: 100%; + overflow-y: auto; border-bottom: 1px solid #ddd; border-right: 1px solid #ddd; flex: 0 1 auto;