diff options
| author | Pierre-Marie Pédrot | 2020-04-10 13:15:01 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-04-10 13:15:01 +0200 |
| commit | 1d7729c1007e320dbae3bc603838da817d40651c (patch) | |
| tree | 9cbef22bc2a2883ca6f56f47ccd0d69c3532fd4f | |
| parent | f373d82ffa7d30df6ace77f7064d4eed6f321b90 (diff) | |
| parent | 00717f0214b3f2f3fbd05848384e33f4e44aa800 (diff) | |
Merge PR #12039: Do not erase native files in debug mode
Reviewed-by: ppedrot
| -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); |
