Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0005397OCamlOCaml generalpublic2011-11-14 09:162013-08-31 12:48
Reporterfrisch 
Assigned Tofrisch 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusclosedResolutionfixed 
PlatformOSOS Version
Product Version 
Target VersionFixed in Version4.00.0+dev 
Summary0005397: Filename.temp_dir_name should be mutable
DescriptionCurrently, Filename.temp_dir_name is obtained from an environment variable when the Filename module is initialized.

It would be convenient to allow changing its value. This would allow some client code to control where third-party libraries, which simply use Filename.temp_file/open_temp_file, put their temp files.

One could add "get_temp_dir_name: unit -> string" and "set_temp_dir_name: string -> unit"; and temp_dir_name would be the original value (marked as deprecated, and removed in a future version).
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2011-11-14 09:16 frisch New Issue
2012-03-26 15:57 lefessan Assigned To => frisch
2012-03-26 15:57 lefessan Status new => acknowledged
2012-03-26 19:29 frisch Status acknowledged => resolved
2012-03-26 19:29 frisch Fixed in Version => 4.00.0+dev
2012-03-26 19:29 frisch Resolution open => fixed
2013-08-31 12:48 xleroy Status resolved => closed


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker