diff options
| author | Pierre-Marie Pédrot | 2018-11-05 11:50:56 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-05 11:50:56 +0100 |
| commit | 3939793d2cb509242cef8c59bdb5cf793af69980 (patch) | |
| tree | ff76955c7b6476f4b52b53db91a8a66d5433be19 /library/libobject.ml | |
| parent | 3517dc938efbc4f7b3c5383bdc5b7e20dc14b2f3 (diff) | |
| parent | e924927fb9d4cf310829c873eaa6c3254238a3ce (diff) | |
Merge PR #8857: [library] Better sizing for libobject hashtbl.
Diffstat (limited to 'library/libobject.ml')
| -rw-r--r-- | library/libobject.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/library/libobject.ml b/library/libobject.ml index ea19fbb90b..43934304c2 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -71,7 +71,7 @@ type dynamic_object_declaration = { let object_tag (Dyn.Dyn (t, _)) = Dyn.repr t let cache_tab = - (Hashtbl.create 17 : (string,dynamic_object_declaration) Hashtbl.t) + (Hashtbl.create 223 : (string,dynamic_object_declaration) Hashtbl.t) let declare_object_full odecl = let na = odecl.object_name in |