diff options
| author | Maxime Dénès | 2020-02-18 13:44:59 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2020-04-07 11:06:01 +0200 |
| commit | 00717f0214b3f2f3fbd05848384e33f4e44aa800 (patch) | |
| tree | 0f708b788f9d58ac7f69aaaa063a30fcc4332316 | |
| parent | 04292ee5af69f168d31345119e25226eadee8ae8 (diff) | |
Do not erase native files in debug mode
Being able to inspect the generated OCaml code is a useful debug tool.
It seems this was disabled by mistake in #11081.
| -rw-r--r-- | kernel/nativelib.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index dde1274152..494282d4e1 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -37,7 +37,7 @@ let ( / ) = Filename.concat let my_temp_dir = lazy (CUnix.mktemp_dir "Coq_native" "") let () = at_exit (fun () -> - if Lazy.is_val my_temp_dir then + if not !Flags.debug && Lazy.is_val my_temp_dir then try let d = Lazy.force my_temp_dir in Array.iter (fun f -> Sys.remove (Filename.concat d f)) (Sys.readdir d); |