indexing

	description: "[

		Implementation of an empty border to avoid a void reference in the widget.

	]"
	date: "$Date$"
	revision: "$Revision$"

class EM_NO_BORDER

inherit

	EM_BORDER

feature -- Drawing

	draw_on (a_widget: EM_WIDGET) is
			-- Draw border on `a_widget'.
		do
		end

invariant

	border_size_zero: top = 0 and left = 0 and right = 0 and bottom = 0

end