5 commits

Author	SHA1	Message	Date
Dan Stillman	5268060802	Move Tools -> Options to Edit -> Preferences on Windows ... Closes #1167	2017-07-18 04:14:17 -04:00
Dan Stillman	cbcfb6b92e	Fix missing Options menu on Windows/Linux	2017-01-10 21:44:03 -05:00
Simon Kornblith	b66c2aab89	Add preferences to menus on Windows and Linux	2012-01-16 21:29:32 -05:00
Simon Kornblith	a35c33312d	Move standalone.dtd out of separate directory	2011-08-10 19:36:05 +00:00
Simon Kornblith	d7e4ae3620	Add some new menu items	2011-06-03 05:14:48 +00:00