aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/nativelib.ml
diff options
context:
space:
mode:
authorGravatar Matej Kosik <matej.kosik@inria.fr>2016-09-28 16:45:55 +0200
committerGravatar Matej Kosik <matej.kosik@inria.fr>2016-09-29 10:22:52 +0200
commit7f96d753d65f7b6fefd725870e1a00f7d942aed7 (patch)
tree618c7cf31d2fbe1bff9df08e13d82298b4ae3bde /kernel/nativelib.ml
parenta75770eb41e8a3bbfb44cb65d04bb3af29448fe7 (diff)
UPDATE: reference to a deprecated variable "Filename.temp_dir_name" was replaced with the recommended "Filename.get_temp_dir_name".
Diffstat (limited to 'kernel/nativelib.ml')
-rw-r--r--kernel/nativelib.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index 1c58c7445..6bd82170e 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -35,7 +35,7 @@ let ( / ) = Filename.concat
(* We have to delay evaluation of include_dirs because coqlib cannot be guessed
until flags have been properly initialized *)
let include_dirs () =
- [Filename.temp_dir_name; coqlib () / "kernel"; coqlib () / "library"]
+ [Filename.get_temp_dir_name (); coqlib () / "kernel"; coqlib () / "library"]
(* Pointer to the function linking an ML object into coq's toplevel *)
let load_obj = ref (fun x -> () : string -> unit)