diff options
| author | Johannes Ranke <jranke@uni-bremen.de> | 2015-12-09 09:19:57 +0100 |
|---|---|---|
| committer | Johannes Ranke <jranke@uni-bremen.de> | 2015-12-09 09:19:57 +0100 |
| commit | 9065639aaa129e309beb80fa5dc0b313461a90f4 (patch) | |
| tree | 4ed1c4626406892c1bf4affa852b75f659ef4a69 /vignettes/gmkin_manual.html | |
| parent | 863b22f40cf81a9ec7271cb4d0fe32e3875f9f42 (diff) | |
Update project explorer selection after confirmation of project switch
When changes of a modified project were dropped during switching a
project, the selection in the project explorer was not updated.
Diffstat (limited to 'vignettes/gmkin_manual.html')
0 files changed, 0 insertions, 0 deletions