This issue tracker is closed. Please visit UPPAAL issue tracker at Github instead.

Bug 412 - Default filename when exporting template
Summary: Default filename when exporting template
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: GUI (show other bugs)
Version: 4.0.5
Hardware: PC Linux
: P2 enhancement
Assignee: Marius Mikučionis
Depends on:
Reported: 2007-04-11 09:29 CEST by Rasmus Jacobsen
Modified: 2007-04-19 18:58 CEST (History)
0 users

See Also:


Note You need to log in before you can comment on or make changes to this bug.
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.