diff options
| author | Enrico Tassi | 2014-12-11 14:28:08 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2014-12-17 15:05:05 +0100 |
| commit | f5a0e2136dacf635c2790099972961b086665a38 (patch) | |
| tree | a1b7dc9ac621f54c158eea92cf569c2f59e676a1 /lib/spawn.ml | |
| parent | 2d66c7d508f6bd198969012241082e34a5b6047c (diff) | |
Spawn: fix request of Gc statistics
Diffstat (limited to 'lib/spawn.ml')
| -rw-r--r-- | lib/spawn.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/spawn.ml b/lib/spawn.ml index 5d5c137c4a..802867e127 100644 --- a/lib/spawn.ml +++ b/lib/spawn.ml @@ -261,7 +261,7 @@ let stats { oob_req; oob_resp; alive } = assert_ alive "This process is dead"; output_value oob_req ReqStats; flush oob_req; - input_value oob_resp + let RespStats g = input_value oob_resp in g let kill_if p ~sec test = T.add_timeout ~sec (fun () -> |