The user opens a new file and then calls "Save as",
inadvertently using the same name as another file
which was already open. No complaints. DrJava saves
it and shows it in the document list with the same
name as the other document!
Log in to post a comment.