Merge lp:~tapaal-contributor/tapaal/disappearing-tokens-1940098 into lp:tapaal
Proposed by
Lena Ernstsen
Status: | Merged | ||||
---|---|---|---|---|---|
Approved by: | Jiri Srba | ||||
Approved revision: | 1136 | ||||
Merged at revision: | 1137 | ||||
Proposed branch: | lp:~tapaal-contributor/tapaal/disappearing-tokens-1940098 | ||||
Merge into: | lp:tapaal | ||||
Diff against target: |
41 lines (+16/-4) 2 files modified
src/dk/aau/cs/gui/SharedPlaceNamePanel.java (+1/-1) src/dk/aau/cs/model/tapn/TimedPlace.java (+15/-3) |
||||
To merge this branch: | bzr merge lp:~tapaal-contributor/tapaal/disappearing-tokens-1940098 | ||||
Related bugs: |
|
Reviewer | Review Type | Date Requested | Status |
---|---|---|---|
Jiri Srba | Approve | ||
Review via email: mp+407251@code.launchpad.net |
Commit message
Stopped tokens from disappearing when shared place names are changed
To post a comment you must log in.
Tested and fixes the problem