diff options
| author | Emilio Jesus Gallego Arias | 2018-10-30 04:03:08 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-31 11:28:14 +0100 |
| commit | e924927fb9d4cf310829c873eaa6c3254238a3ce (patch) | |
| tree | 23e205cca5742557e8352a15245816451c7eb902 /library/libobject.ml | |
| parent | 310f8fa900bc0d25a05f6409d941708a74aca60b (diff) | |
[library] Better sizing for libobject hashtbl.
17 is a very small number as files in the stdlib will routinely pass
size 190.
As this is done only on startup, it seems wise to provide a bit more
space.
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 79a3fed1b9..c3b96d11fc 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -65,7 +65,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 |