From 1256d13869af4c65e90c6ad1d96ee0e2941cba9f Mon Sep 17 00:00:00 2001
From: yann300 <yann.levreau@gmail.com>
Date: Thu, 9 May 2019 10:38:44 +0200
Subject: [PATCH] add padding to the filter input in terminal

---
 src/app/panels/styles/terminal-styles.js | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/app/panels/styles/terminal-styles.js b/src/app/panels/styles/terminal-styles.js
index 61776b74e0..968411bcd6 100644
--- a/src/app/panels/styles/terminal-styles.js
+++ b/src/app/panels/styles/terminal-styles.js
@@ -93,6 +93,8 @@ var css = csjs`
     width             : 330px;
     padding-left      : 20px;
     height            : 100%;
+    padding-top       : 1px;
+    padding-bottom    : 1px;
   }
   .filter                       {
     padding-right               : 0px;