diff options
author | 2017-11-19 03:27:46 +0100 | |
---|---|---|
committer | 2017-11-19 03:28:53 +0100 | |
commit | d7a5f439de0208c4a543a81158107b8ccecb6ced (patch) | |
tree | f600915d5c97799bb59fd370049cb5ecc55ae9eb /engine/namegen.ml | |
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 'engine/namegen.ml')
0 files changed, 0 insertions, 0 deletions