diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-12-11 14:28:08 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-12-17 15:05:05 +0100 |
| commit | f5a0e2136dacf635c2790099972961b086665a38 (patch) | |
| tree | a1b7dc9ac621f54c158eea92cf569c2f59e676a1 /stm/spawned.ml | |
| parent | 2d66c7d508f6bd198969012241082e34a5b6047c (diff) | |
Spawn: fix request of Gc statistics
Diffstat (limited to 'stm/spawned.ml')
| -rw-r--r-- | stm/spawned.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/stm/spawned.ml b/stm/spawned.ml index 21902f71d..e2d07ef5b 100644 --- a/stm/spawned.ml +++ b/stm/spawned.ml @@ -44,7 +44,7 @@ let controller h p = | Hello _ -> prerr_endline "internal protocol error"; exit 1 | ReqDie -> prerr_endline "death sentence received"; exit 0 | ReqStats -> - output_value oc (RespStats (Gc.stat ())); flush oc; loop () + output_value oc (RespStats (Gc.quick_stat ())); flush oc; loop () with | e -> prerr_endline ("control channel broken: " ^ Printexc.to_string e); |