~tapaal-contributor/tapaal/fix-tikz-export-1945642

Changed unit from px to pt

added added

removed removed

478

private StringBuffer exportTikZstyle() {

479

StringBuffer out = new StringBuffer();

480

481

out.append("\\begin{tikzpicture}[font=\\scriptsize, xscale=0.45, yscale=0.45, x=1.33px, y=1.33px]\n");

481

out.append("\\begin{tikzpicture}[font=\\scriptsize, xscale=0.45, yscale=0.45, x=1.33pt, y=1.33pt]\n");

482

out.append("%% the figure can be scaled by changing xscale and yscale\n");

483

out.append("%% positions of place/transition labels that are currently fixed to label=135 degrees\n");

484

out.append("%% can be adjusted so that they do not cover arcs\n");