diff options
| author | Emilio Jesus Gallego Arias | 2018-08-29 14:42:30 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-08-29 14:42:30 +0200 |
| commit | ccb6729593cd35d9c1cfa680927f15cda635ad8f (patch) | |
| tree | dc1dd3529665f09196de8742d46254cdcb2fd0c6 | |
| parent | ba256907542d3ada8c824e535b2ba243c5bf7529 (diff) | |
| parent | e00dc32b1d533859a023834f91ede66f5240ad5a (diff) | |
Merge PR #8350: Fix typo in comment, sollicited --> solicited.
| -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 9b68f303a6..bdd33e10ef 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -384,7 +384,7 @@ let print_style_tags opts = (** GC tweaking *) (** Coq is a heavy user of persistent data structures and symbolic ASTs, so the - minor heap is heavily sollicited. Unfortunately, the default size is far too + minor heap is heavily solicited. Unfortunately, the default size is far too small, so we enlarge it a lot (128 times larger). To better handle huge memory consumers, we also augment the default major |