DrJava / Bugs / #912 Right margin is not visible

A lightweight programming environment for Java

#912 Right margin is not visible

Milestone: 1: Would be nice if fixed ...

Status: closed-fixed

Owner: Mathias Ricken

Labels: User interface (128)

Priority: 5

Updated: 2011-08-11

Created: 2011-08-08

Creator: Anonymous

Private: No

The right margin never appears. I've tried turning it on/off, changing the color, changing the location (120, 80, 70), trying the latest stable and development Windows exe versions of Dr. Java, as well as the July 27 .jar version. The right margin guide quite simply has never appeared.

Discussion

Mathias Ricken - 2011-08-08

Thanks for pointing this out. We've had a regression somewhere. I haven't found it yet, though.

If you would like to refer to this comment somewhere else in this project, copy and paste the following link:

Mathias Ricken - 2011-08-08

status: open --> open-accepted
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:

Mathias Ricken - 2011-08-11

assigned_to: nobody --> mgricken

status: open-accepted --> closed-fixed
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:

Mathias Ricken - 2011-08-11

Fixed as of revision 5438.

You can download a weekly release from http://www.cs.rice.edu/~javaplt/drjavarice/weekly/

If you would like to refer to this comment somewhere else in this project, copy and paste the following link:

Right margin is not visible

A lightweight programming environment for Java

Group

Searches

Help

#912 Right margin is not visible

Discussion