[DrJava] [ drjava-Ease of use Issues-788303 ] Change EOI comments in history

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

Ease of use Issues item #788303, was opened at 2003-08-13 20:07
Message generated for change (Tracker Item Submitted) made by Item Submitter
You can respond by visiting: 
https://sourceforge.net/tracker/?func=detail&atid=460211&aid=788303&group_id=44253

Category: Platform Independent
Group: None
Status: Open
Resolution: None
Priority: 5
Submitted By: Charles Reis (csreis)
Assigned to: Nobody/Anonymous (nobody)
Summary: Change EOI comments in history

Initial Comment:
In drjava-20030812-2156, each line of an interactions
history is terminated by "//EOI//", which is visible
when editing the history before saving it.

This is up for debate, but I think it might be better
to use something like:
int x = 3;/*End of Interaction*/

I don't think the extra characters are going to make
that big a difference, since histories don't typically
get very large, and it would be much clearer to the
user why that comment is there.

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

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