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
Status: RESOLVED FIXED
Alias: None
Product: UPPAAL
Classification: Unclassified
Component: GUI (show other bugs)
Version: 4.0.5
Hardware: PC Linux
: P2 enhancement
Assignee: Marius Mikučionis
URL:
Depends on:
Blocks:
 
Reported: 2007-04-11 09:29 CEST by Rasmus Jacobsen
Modified: 2007-04-19 18:58 CEST (History)
0 users

See Also:
Architecture:

Attachments
Add an attachment (proposed patch, testcase, etc.)

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.