Description Martin Aeschlimann 2003-09-17 08:49:50 EDT

20020917


line 94 should check if the buffer isn't the same: In the case of saving a 
primary working copy, the buffer from the original is identical to the buffer 
of the working copy
if (workingCopyBuffer != primaryBuffer) {
  primaryBuffer.setContents(workingCopyBuffer.getCharacters());
}