-
Committer:
Jiri Srba
-
Date:
2018-08-14 13:06:51 UTC
-
mfrom:
(974.1.2 tapaal)
-
Revision ID:
srba@cs.aau.dk-20180814130651-e18hqqau9axoml3i
merged in branch lp:~tapaal-contributor/tapaal/highlight-names-on-select-1786755
that highlights names of selected places and transitions