Handbook
Glossary
margins ( child -- border )
Vocabulary
ui
.
tools
.
common
Inputs
child
an
object
Outputs
border
an
object
Definition
USING:
ui.gadgets.borders
;
IN:
ui.tools.common
:
margins
( child -- border )
{
9 9
}
<filled-border>
;