Highlight place/transition names when selected
Bug #1786755 reported by
Jiri Srba
This bug affects 1 person
| Affects | Status | Importance | Assigned to | Milestone | |
|---|---|---|---|---|---|
| TAPAAL |
Fix Released
|
Critical
|
Peter Haahr Taankvist | ||
Bug Description
In editor when a place or transition is selected, its name (and possibly place invariant)
should be highlighed too (as it is now done for arcs).
Related branches
lp:~tapaal-contributor/tapaal/highlight-names-on-select-1786755
- Jiri Srba: Approve
- Peter Haahr Taankvist (community): Needs Resubmitting
-
Diff: 29 lines (+4/-0)2 files modifiedsrc/pipe/gui/graphicElements/Place.java (+2/-0)
src/pipe/gui/graphicElements/Transition.java (+2/-0)
| Changed in tapaal: | |
| status: | New → Fix Committed |
| Changed in tapaal: | |
| status: | Fix Committed → Fix Released |
To post a comment you must log in.
