From 937e59d0f778417455a161bd1f74b2ebf415a0e3 2015-01-19 17:41:32
From: Jonathan Frederic <jon.freder@gmail.com>
Date: 2015-01-19 17:41:32
Subject: [PATCH] Use less for heading padding

---

diff --git a/IPython/html/static/tree/less/tree.less b/IPython/html/static/tree/less/tree.less
index ad10a93..fc34736 100644
--- a/IPython/html/static/tree/less/tree.less
+++ b/IPython/html/static/tree/less/tree.less
@@ -187,10 +187,10 @@ ul#new-menu {
 
             .panel-heading {
                 background-color: #eee; /* @page-backdrop-color */
-                padding-top: 4px;
-                padding-bottom: 4px;
-                padding-left: 7px;
-                padding-right: 7px;
+                padding-top: @dashboard_tb_pad;
+                padding-bottom: @dashboard_tb_pad;
+                padding-left: @dashboard_lr_pad;
+                padding-right: @dashboard_lr_pad;
             }
 
             .panel-body {