diff options
| author | bors[bot] <bors[bot]@users.noreply.github.com> | 2019-05-13 21:23:09 +0100 |
|---|---|---|
| committer | bors[bot] <bors[bot]@users.noreply.github.com> | 2019-05-13 21:23:09 +0100 |
| commit | d7a4ae43f9308f683ddb3ca89104c5eb12d8d6b3 (patch) | |
| tree | a8dfca16f08dff9b5a360b91e2a233bd6820267d /editors | |
| parent | 033a32f34944d7e07facd900a78db59b35e6698c (diff) | |
| parent | c29a692137f2db4522f1b97d4e058757b82b973b (diff) | |
Merge #1270
1270: Increase Chalk solver max_size back to 4 r=flodiebold a=flodiebold
Reducing it to 2 was just a failed attempt to see whether that would help fix
some slow cases; in fact, it can create new slow cases by replacing concrete
types by variables.
Co-authored-by: Florian Diebold <[email protected]>
Diffstat (limited to 'editors')
0 files changed, 0 insertions, 0 deletions