DrJava

Tracker: Support Requests

1 Eclipse plug-in: set font? - ID: 928380

Last Update: Comment added ( csreis )

Details:

How do I set the font for the interactions pane of the Eclipse
plug-in? Supposedly the 0.9.3 release allows the user to set
the font, but there's no option for it in the DrJava
preferences page.

-- Eric

Submitted:

Eric E. Allen ( eallen ) - 2004-04-02 17:08

Priority:

Status:

Closed

Resolution:

None

Assigned:

Charles Reis

Category:

Other

Group:

None

Visibility:

Public

Comment ( 1 )

Date: 2004-04-02 17:15 Sender: csreis Logged In: YES user_id=429731 It's actually with all the other font preferences, which are in the Workbench/Fonts page. (I agree that it isn't quite as easy to find if you're thinking about the Interactions pane, but it is consistent with the way they handle fonts for everything else.) Charlie

Log in to comment.

Attached File

Changes ( 3 )

Field	Old Value	Date	By
status_id	Open	2004-04-02 17:15	csreis
assigned_to	nobody	2004-04-02 17:15	csreis
close_date	-	2004-04-02 17:15	csreis

DrJava

Tracker: Support Requests

Comment ( 1 )

Log in to comment.

Attached File

No Files Currently Attached

Changes ( 3 )

About SourceForge

Find Software

Develop Software

Community

Help