Simon Michael 42a4a4a7e4 ui: use "border" instead of borderAttr everywhere ... Assume it won't change, it's clearer and more consistent.		2018-10-23 06:43:21 -07:00
..
UI	ui: use "border" instead of borderAttr everywhere	2018-10-23 06:43:21 -07:00
UI.hs	ui, web: fix build after tests cleanup	2018-09-03 08:43:57 -07:00