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
|
