Re: [ jEdit-devel ] [ jedit-Bugs-443401 ] File System Browser not configurable

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