Re: [GITGRUB] New menu interface (implementation)

[Michal Suchanek]

2009/10/7 Bean <address@hidden>:
> On Wed, Oct 7, 2009 at 4:54 PM, Michal Suchanek <address@hidden> wrote:
>> This might make switching the direction of a panel more difficult but
>> there may be other issues. Either way the method with margin does not
>> work either.
>
> Hi,
>
> The latest version should work now, although there is a small issue,
> the margin_*, padding_* property only works for panel widget for now,
> so you should replace padding_* of the term with margin_* of parent
> panel.

Yes, spacing on panels should be sufficient.

Terminals probably would not have borders and such anyway.

Thanks

Michal