Tue, 10 Aug 2010 12:09:53 +0200 | wenzelm | added Library.thread_actor -- thread as actor; | changeset | files |
Tue, 10 Aug 2010 12:08:24 +0200 | wenzelm | clarified JEDIT_JAVA_OPTIONS vs. JEDIT_SYSTEM_OPTIONS -- discontinued JEDIT_APPLE_PROPERTIES; | changeset | files |