HEAD - Fix for 362711: possibly incorrect JDT POST_CHANGE event fired when a
file is replaced
5 files changed