daily pastebin goal
75%
SHARE
TWEET

Untitled

a guest Feb 16th, 2019 82 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
  1. From 3cccfc5ff56b882a890587aad1c2cab772b39fd6 Mon Sep 17 00:00:00 2001
  2. From: Jeremie Dimino <jdimino@janestreet.com>
  3. Date: Fri, 15 Mar 2013 16:58:46 +0000
  4. Subject: [PATCH] handle EINTR in Unix.system
  5.  
  6. ---
  7.  otherlibs/unix/unix.ml |   10 +++++-----
  8.  1 files changed, 5 insertions(+), 5 deletions(-)
  9.  
  10. diff --git a/otherlibs/unix/unix.ml b/otherlibs/unix/unix.ml
  11. index 8e573d8..8a69ca7 100644
  12. --- a/otherlibs/unix/unix.ml
  13. +++ b/otherlibs/unix/unix.ml
  14. @@ -837,6 +837,10 @@ external setsid : unit -> int = "unix_setsid"
  15.  
  16.  (* High-level process management (system, popen) *)
  17.  
  18. +let rec waitpid_non_intr pid =
  19. +  try waitpid [] pid
  20. +  with Unix_error (EINTR, _, _) -> waitpid_non_intr pid
  21. +
  22.  let system cmd =
  23.    match fork() with
  24.       0 -> begin try
  25. @@ -844,7 +848,7 @@ let system cmd =
  26.            with _ ->
  27.              exit 127
  28.            end
  29. -  | id -> snd(waitpid [] id)
  30. +  | id -> snd(waitpid_non_intr id)
  31.  
  32.  let rec safe_dup fd =
  33.    let new_fd = dup fd in
  34. @@ -997,10 +1001,6 @@ let find_proc_id fun_name proc =
  35.    with Not_found ->
  36.      raise(Unix_error(EBADF, fun_name, ""))
  37.  
  38. -let rec waitpid_non_intr pid =
  39. -  try waitpid [] pid
  40. -  with Unix_error (EINTR, _, _) -> waitpid_non_intr pid
  41. -
  42.  let close_process_in inchan =
  43.    let pid = find_proc_id "close_process_in" (Process_in inchan) in
  44.    close_in inchan;
  45. --
  46. 1.7.1
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy. OK, I Understand
 
Top