diff options
| author | Emilio Jesus Gallego Arias | 2017-11-19 03:27:46 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-11-19 03:28:53 +0100 |
| commit | d7a5f439de0208c4a543a81158107b8ccecb6ced (patch) | |
| tree | f600915d5c97799bb59fd370049cb5ecc55ae9eb /API/API.mli | |
| parent | edf1a8f36f75861b822081b3825357e122b6937d (diff) | |
[vernac] Increase table size.
As of Nov 2017, the standard number of entries is 85, it easily goes
up with some other plugins, so 211 seems like a good compromise.
Diffstat (limited to 'API/API.mli')
0 files changed, 0 insertions, 0 deletions