2009/10/7 Bean <bean12...@gmail.com>: > On Wed, Oct 7, 2009 at 4:54 PM, Michal Suchanek <hramr...@centrum.cz> 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 Grub-devel@gnu.org http://lists.gnu.org/mailman/listinfo/grub-devel
