Viewing all changes in revision 994.
- Committer: Jiri Srba
- Date: 2019-03-15 19:06:43 UTC
- mfrom: (993.1.1 tapaal)
- Revision ID: srba@cs.aau.dk-20190315190643-a2oqyordw12gtthy
merged in branch lp:~tapaal-contributor/tapaal/change-export-batch-shortcut-1820012 that fixed hot-key for batch export to PNML/XML
- files modified:
- src/pipe/gui/GuiFrame.java
expand all
collapse all
added
removed
