| commit | 573fa3ee777239ae00ea883f701613bfad0e3a1d | [log] [tgz] |
|---|---|---|
| author | mjger <michael.oberlehner@jku.at> | Mon Apr 26 18:03:37 2021 +0200 |
| committer | Michael Oberlehner <michael.oberlehner@jku.at> | Tue Apr 27 13:45:39 2021 -0500 |
| tree | e715dfb100b4e46d66e787f35b5de2a68d420a33 | |
| parent | 6166bdb0d841fb31d5dfd786389a67cf9a776cc5 [diff] |
[573173] Make workspace refresh on start up The refresh of the workspace, which ensure a NOT dirty workspace is now at the start up phase in 4diac. The previous version has triggered the resource change listener, which also accesses the same type library and throws concurrent modification exceptions. Bug: https://bugs.eclipse.org/bugs/show_bug.cgi?id=573173 Change-Id: I10d458124b0d5d33060e33ed896e992b03cb9c13