← Back to branch summary

~tapaal-contributor/tapaal/disappearing-tokens-1940098

« back to all changes in this revision

Viewing changes to src/pipe/gui/GuiFrame.java

  • Committer: Jiri Srba
  • Date: 2020-12-16 08:38:28 UTC
  • Revision ID: srba@cs.aau.dk-20201216083828-wwucqt2eo0yzgo2f
fixed a tooltip for batch export menu item

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/pipe/gui/GuiFrame.java
176
176
            currentTab.ifPresent(TabContentActions::importTrace);
177
177
        }
178
178
    };
179
 
    private final GuiAction exportBatchAction = new GuiAction("Batch Export of model and queries", "Export multiple nets into PNML together with the XML queries, while removing the timing information", KeyStroke.getKeyStroke('D', (shortcutkey + InputEvent.SHIFT_DOWN_MASK))) {
 
179
    private final GuiAction exportBatchAction = new GuiAction("Batch Export of model and queries", "Export multiple nets and queries for the command line use with the verification engines.", KeyStroke.getKeyStroke('D', (shortcutkey + InputEvent.SHIFT_DOWN_MASK))) {
180
180
        public void actionPerformed(ActionEvent e) {
181
181
            ExportBatchDialog.ShowExportBatchDialog();
182
182
        }