|Summary:||Default filename when exporting template|
|Product:||UPPAAL||Reporter:||Rasmus Jacobsen <rasseren>|
|Component:||GUI||Assignee:||Marius Mikučionis <marius>|
Description Rasmus Jacobsen 2007-04-11 09:29:08 CEST
Hi again It would be nice if the name of the template was entered as default filename when exporting to eps. Thanks Rasmus
Comment 1 Gerd Behrmann 2007-04-11 12:43:33 CEST
Agreed. I think this change is minor enough, yet very useful, to allow it to be done on the stable branch. Marius, do you do it?
Comment 2 Marius Mikučionis 2007-04-11 19:33:08 CEST
here, you have it in branch/4.0 :-) now it dumps the picture to template.eps instead of stdout. shall I update the trunk too?
Comment 3 Marius Mikučionis 2007-04-19 18:58:56 CEST
it seems that version at trunk requires an explicit option for the filename, so I declare this bug as fixed.