From a0bc13846556ad8d8c3c7ed30277805f5b330852 Mon Sep 17 00:00:00 2001
From: nicolas-p <z.nicolas@gmail.com>
Date: Sat, 18 Jul 2015 16:48:47 +0200
Subject: [PATCH] Menu border
Added 3 px to menu borders.
---
basis/ui/gadgets/menus/menus.factor | 1 +
1 file changed, 1 insertion(+)
diff --git a/basis/ui/gadgets/menus/menus.factor b/basis/ui/gadgets/menus/menus.factor
index d7a63dd3c9..6d329a5554 100644
--- a/basis/ui/gadgets/menus/menus.factor
+++ b/basis/ui/gadgets/menus/menus.factor
@@ -33,6 +33,7 @@ M: separator-pen draw-interior
: <menu-items> ( items -- gadget )
[ <filled-pile> ] dip add-gadgets
+ { 3 3 } <border>
panel-background-color <solid> >>interior ;
PRIVATE>