diff options
| author | Guillaume Melquiond | 2015-12-31 17:02:00 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2015-12-31 17:02:00 +0100 |
| commit | 5319465eb1eaf89410dac96cd14b14b9b95601e7 (patch) | |
| tree | b52306041b4351e6a01984d391da3a82af82ec11 /lib | |
| parent | 1a157442dff4bfa127af467c49280e79889acde7 (diff) | |
| parent | d3bc575c498ae09ad1003405d17a9d5cfbcf3cbf (diff) | |
Merge branch 'v8.5' into trunk
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/loc.ml | 2 | ||||
| -rw-r--r-- | lib/spawn.ml | 8 |
2 files changed, 7 insertions, 3 deletions
diff --git a/lib/loc.ml b/lib/loc.ml index b62677d484..9043bee075 100644 --- a/lib/loc.ml +++ b/lib/loc.ml @@ -31,7 +31,7 @@ let ghost = { fname = ""; line_nb = -1; bol_pos = 0; line_nb_last = -1; bol_pos_last = 0; bp = 0; ep = 0; } -let is_ghost loc = Pervasives.(=) loc ghost (** FIXME *) +let is_ghost loc = loc.ep = 0 let merge loc1 loc2 = if loc1.bp < loc2.bp then diff --git a/lib/spawn.ml b/lib/spawn.ml index 851c6a2235..01f6a4f8d3 100644 --- a/lib/spawn.ml +++ b/lib/spawn.ml @@ -175,7 +175,7 @@ let is_alive p = p.alive let uid { pid; } = string_of_int pid let unixpid { pid; } = pid -let kill ({ pid = unixpid; oob_req; cin; cout; alive; watch } as p) = +let kill ({ pid = unixpid; oob_resp; oob_req; cin; cout; alive; watch } as p) = p.alive <- false; if not alive then prerr_endline "This process is already dead" else begin try @@ -183,6 +183,8 @@ let kill ({ pid = unixpid; oob_req; cin; cout; alive; watch } as p) = output_death_sentence (uid p) oob_req; close_in_noerr cin; close_out_noerr cout; + close_in_noerr oob_resp; + close_out_noerr oob_req; if Sys.os_type = "Unix" then Unix.kill unixpid 9; p.watch <- None with e -> prerr_endline ("kill: "^Printexc.to_string e) end @@ -247,13 +249,15 @@ let is_alive p = p.alive let uid { pid; } = string_of_int pid let unixpid { pid = pid; } = pid -let kill ({ pid = unixpid; oob_req; cin; cout; alive } as p) = +let kill ({ pid = unixpid; oob_req; oob_resp; cin; cout; alive } as p) = p.alive <- false; if not alive then prerr_endline "This process is already dead" else begin try output_death_sentence (uid p) oob_req; close_in_noerr cin; close_out_noerr cout; + close_in_noerr oob_resp; + close_out_noerr oob_req; if Sys.os_type = "Unix" then Unix.kill unixpid 9; with e -> prerr_endline ("kill: "^Printexc.to_string e) end |