Viewing all changes in revision 1101.
- Committer: Jiri Srba
- Date: 2020-09-16 19:30:40 UTC
- mfrom: (1099.2.1 fix1894107-mouseWheelOnPTO)
- Revision ID: srba@cs.aau.dk-20200916193040-3sh8xstior7elf2n
merged in lp:~yrke/tapaal/fix1894107-mouseWheelOnPTO fixing accidental rotation of transitions and adding tokens to places - now it is enabled only if the places/transition is selected
- files modified:
- src/dk/aau/cs/gui/TabContent.java
expand all
collapse all
added
removed
