Path: news.easynews.com!easynews!sn-xit-02!supernews.com!postnews1.google.com!not-for-mail
From: ligart@yahoo.com (Ladislav Ligart)
Newsgroups: comp.databases.oracle.tools
Subject: Re: how to change MENU font size in JDeveloper 9i?
Date: 12 Apr 2002 12:06:04 -0700
Organization: http://groups.google.com/
Lines: 4
Message-ID: <ed51c2ec.0204121106.2f15789f@posting.google.com>
References: <ed51c2ec.0204091130.7f4dd2e7@posting.google.com>
NNTP-Posting-Host: 63.141.35.126
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: 8bit
X-Trace: posting.google.com 1018638364 30923 127.0.0.1 (12 Apr 2002 19:06:04 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: 12 Apr 2002 19:06:04 GMT
Xref: easynews comp.databases.oracle.tools:50624
X-Received-Date: Fri, 12 Apr 2002 12:03:47 MST (news.easynews.com)

For anyone who cares, you can change the system font size by editing
the ide.properties file located in the jdev/system folder. You can
change it on a global, per language, or per look-and-feel basis
(there's lots of comments in the file itself).