diff options
| author | coqbot-app[bot] | 2020-11-21 17:33:44 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-21 17:33:44 +0000 |
| commit | 9d36da17138d9117e0582f65c9f70e696c7bcc94 (patch) | |
| tree | a492b0e49a1114c9987b2c97e0710701a1d99d6b /plugins | |
| parent | 5b15fce17d856dfbd51482f724ddf5e5f9646073 (diff) | |
| parent | 8e152ab7156c6c642bb4665d4610cc8c49242141 (diff) | |
Merge PR #13431: Make sure accumulators do not exceed the minor heap (partly fix #11170).
Reviewed-by: gares
Reviewed-by: xavierleroy
Ack-by: ppedrot
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions