From 265a855217dd091a4c0b9fc9682f286f8360563b Mon Sep 17 00:00:00 2001
From: nicolas-p <z.nicolas@gmail.com>
Date: Sun, 19 Jul 2015 22:29:47 +0200
Subject: [PATCH] Common margins for all panes

(Is this the right place to put it?)
---
 basis/ui/tools/common/common.factor | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/basis/ui/tools/common/common.factor b/basis/ui/tools/common/common.factor
index 03b1eeb783..5ad2d68357 100644
--- a/basis/ui/tools/common/common.factor
+++ b/basis/ui/tools/common/common.factor
@@ -38,3 +38,6 @@ SLOT: scroller
 
 : com-scroll-down ( tool -- )
     scroller>> scroll-down-line ;
+
+: margins ( child -- border ) 
+    { 9 9 } <filled-border> ;