Viewing all changes in revision 1057.
- Committer: Mads Johannsen
- Date: 2017-08-13 17:52:38 UTC
- Revision ID: mjohan12@student.aau.dk-20170813175238-kvkhhzjjgtroc81x
Hide mouse hover window in animation mode for places and transitions
- files modified:
- src/pipe/gui/GuiFrame.java
expand all
collapse all
added
removed
