← Back to branch summary

~tapaal-contributor/tapaal/ImpossibleToDeletePlace-1826206

« back to all changes in this revision

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

  • Committer: Jiri Srba
  • Date: 2019-03-15 19:09:57 UTC
  • mfrom: (993.2.1 tapaal)
  • Revision ID: srba@cs.aau.dk-20190315190957-xsjcveedvbinv0wl
merged in branch lp:~tapaal-contributor/tapaal/make-grid-reappear-on-export-tikz-cancel-1820016 that fixes problem with disappearing grid after cancelled export to tikz

Show diffs side-by-side

added added

removed removed

Lines of Context:
src/pipe/gui/Export.java
241
241
                                                null, possibilities, "Only the TikZ figure");
242
242
                                TikZExporter.TikZOutputOption tikZOption = TikZExporter.TikZOutputOption.FIGURE_ONLY;
243
243
                                if (figureOptions == null)
244
 
                                        return;
 
244
                                        break;
245
245
 
246
246
                                if (figureOptions == possibilities[0])
247
247
                                        tikZOption = TikZExporter.TikZOutputOption.FIGURE_ONLY;