John Benediktsson f7d92e4712 ui.tools.listener: fix introduction font sizes. ... (should be smaller than default-style)		2016-04-29 18:30:59 -07:00
..
browser	ui.gadgets.editors: make it easier to set and get default-text.	2015-08-16 14:29:21 -07:00
common	ui.gadgets.colors moved to ui.gadgets.theme	2015-08-16 07:53:33 -07:00
debugger	Fix comments to be ! not #!.	2015-09-08 16:15:10 -07:00
deploy	…
error-list	Fix comments to be ! not #!.	2015-09-08 16:15:10 -07:00
inspector	ui.gadgets.colors moved to ui.gadgets.theme	2015-08-16 07:53:33 -07:00
listener	ui.tools.listener: fix introduction font sizes.	2016-04-29 18:30:59 -07:00
operations	…
traceback	ui.gadgets.colors moved to ui.gadgets.theme	2015-08-16 07:53:33 -07:00
walker	ui.tools.walker: improved status text	2015-08-16 07:54:45 -07:00
authors.txt	…
summary.txt	…
tags.txt	…
tools-docs.factor	…
tools.factor	…