From 1d637f15de540c82289d6b3a16181a625a0d9cdf Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 4 Nov 2016 13:28:08 +0100
Subject: Fix #4837: ./configure -local makes coqdep issue many warnings

We simply remove the warnings about paths mixing Win32 and Unix
separators, since that situation does not seem problematic (c.f.
discussion on the bug tracker).
---
 lib/system.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'lib/system.ml')

diff --git a/lib/system.ml b/lib/system.ml
index af9aa5c074..4b99de707b 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -33,7 +33,6 @@ let all_subdirs ~unix_path:root =
       | _ -> ()
     in process_directory f path
   in
-  check_unix_dir (fun s -> Feedback.msg_warning (str s)) root;
   if exists_dir root then traverse root []
   else warn_cannot_open_dir root;
   List.rev !l
-- 
cgit v1.2.3


From 6424a49842ed9982c7edd1b847d88d66508f072b Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 11 Jan 2017 13:59:54 +0100
Subject: Fix race condition in STM DAG generation (in debug mode).

The same file name for .dot graphs could be used by concurrent processes.
---
 lib/system.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'lib/system.ml')

diff --git a/lib/system.ml b/lib/system.ml
index 4b99de707b..1817aed1fc 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -309,6 +309,7 @@ let with_time time f x =
     raise e
 
 let process_id () =
-  if Flags.async_proofs_is_worker () then !Flags.async_proofs_worker_id
-  else Printf.sprintf "master:%d" (Thread.id (Thread.self ()))
-    
+  Printf.sprintf "%d:%s:%d" (Unix.getpid ())
+    (if Flags.async_proofs_is_worker () then !Flags.async_proofs_worker_id
+     else "master")
+    (Thread.id (Thread.self ()))
-- 
cgit v1.2.3