[DrJava] [ drjava-Bugs-853339 ] Can't change fonts in Interactions pane

[SourceForge.net <no...@so...>]

Bugs item #853339, was opened at 2003-12-03 10:10
Message generated for change (Tracker Item Submitted) made by Item Submitter
You can respond by visiting: 
https://sourceforge.net/tracker/?func=detail&atid=438935&aid=853339&group_id=44253

Category: Eclipse Plug-in
Group: Ugly
Status: Open
Resolution: None
Priority: 5
Submitted By: William Pugh (wpugh)
Assigned to: Nobody/Anonymous (nobody)
Summary: Can't change fonts in Interactions pane

Initial Comment:
Using the DrJava plugin in Eclipse 3.0m5, I am unable to 
change the font in the interaction pane. To use the DrJava 
plug in in a course, we really need to be able to make the 
font size larger.

----------------------------------------------------------------------

You can respond by visiting: 
https://sourceforge.net/tracker/?func=detail&atid=438935&aid=853339&group_id=44253