From 3dc104d11e3a76ce077ba795e7392b02c4eff107 Mon Sep 17 00:00:00 2001 From: yann300 Date: Thu, 4 Apr 2019 19:54:57 +0200 Subject: [PATCH] fix terminal minimzing --- src/app/panels/editor-panel.js | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/app/panels/editor-panel.js b/src/app/panels/editor-panel.js index 91c4810042..206ef8ab80 100644 --- a/src/app/panels/editor-panel.js +++ b/src/app/panels/editor-panel.js @@ -127,7 +127,7 @@ class EditorPanel { if (delta === undefined) { layout.show = !layout.show if (layout.show) delta = layout.offset - else delta = containerHeight + else delta = 0 } else { layout.show = true self._deps.config.set(`terminal-${direction}-offset`, delta)