|
From: Slava P. <sl...@je...> - 2001-07-31 07:47:44
|
On Mon, Jul 30, 2001 at 10:54:33PM -0700, no...@so... wrote: > >Comment By: Dirk M=F6bius (dmoebius) > Date: 2001-07-30 22:54 >=20 > Message: > Logged In: YES=20 > user_id=3D9521 >=20 > Does anybody have an updated script for 3.2pre6? If someone sends me a version of this script that works with 3.2 (don't forget that several components that previously had hard-coded fonts, such as the buffer switcher, now use the Swing default font in 3.2, so the script can be simplified) I will include it in the 'startup' directory, probably commented out. Then savvy users who discover it can uncomment the code to tweak their fonts. This will only be a short-term solution until jEdit 4.0. Slava |