diff options
| author | Pierre-Marie Pédrot | 2020-07-11 13:23:02 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-07-11 13:23:02 +0200 |
| commit | c412b32707a296a6b17292782ed1194413353387 (patch) | |
| tree | f0da25ea7f42533e3bd1ef1e2f94fb5ebd33af7e /toplevel | |
| parent | 7e149d3e7c7c6690b6aa92887d28e42f997b148a (diff) | |
| parent | 2b877400967387a5364c1e630c91efacae3c7c8a (diff) | |
Merge PR #12635: Correct comment and clarify constant
Reviewed-by: ppedrot
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqtop.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 4231915be1..bbcfcc4826 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -161,7 +161,7 @@ let init_gc () = * In this case, we put in place our preferred configuration. *) Gc.set { (Gc.get ()) with - Gc.minor_heap_size = 33554432; (* 4M *) + Gc.minor_heap_size = 32*1024*1024; (* 32Mwords x 8 bytes/word = 256Mb *) Gc.space_overhead = 120} let init_process () = |