3 commits

Author	SHA1	Message	Date
Christoph Oelckers	a08cc2b477	- switched the input grid to the new font. Also use the same scale as the rest of the menus.	2019-03-31 10:08:09 +02:00
Alexander	dbb93d6c08	option search improvements ... 1. Top-level menu names are now properly handled. 2. Changing "Any or All terms" option now immediately updates the results. 3. Reformatted menu.zs to have tabs instead of spaces.	2019-03-17 20:28:38 +01:00
Alexander	73d81d3983	added option search menu	2019-03-16 18:40:13 +01:00