Join GitHub today
GitHub is home to over 31 million developers working together to host and review code, manage projects, and build software together.Sign up
Filename.temp_dir_name should be mutable #5397
Original bug ID: 5397
Currently, 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).