John Benediktsson b90f37b13e ui.tools.common: only save tool-dim when not fullscreen.		2017-10-25 16:16:53 -07:00
..
common-docs.factor	ui.tools.*: fix swapped argument order for set-tool-dim	2016-07-30 19:03:23 +02:00
common.factor	ui.tools.common: only save tool-dim when not fullscreen.	2017-10-25 16:16:53 -07:00