2009/10/7 Bean <[email protected]>: > On Wed, Oct 7, 2009 at 4:54 PM, Michal Suchanek <[email protected]> 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 _______________________________________________ Grub-devel mailing list [email protected] http://lists.gnu.org/mailman/listinfo/grub-devel
