diff options
Diffstat (limited to 'stdlib/gc.ml')
| -rw-r--r-- | stdlib/gc.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/stdlib/gc.ml b/stdlib/gc.ml index 29ae1f837..d654fff29 100644 --- a/stdlib/gc.ml +++ b/stdlib/gc.ml @@ -32,7 +32,7 @@ type control = { mutable minor_heap_size : int; mutable major_heap_increment : int; mutable space_overhead : int; - mutable verbose : bool; + mutable verbose : int; mutable max_overhead : int; mutable stack_limit : int };; |