diff options
| author | Emilio Jesus Gallego Arias | 2020-07-15 13:14:34 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-07-15 13:14:34 +0200 |
| commit | 782173c2a53196cadae8b99abe65df08552c6ce1 (patch) | |
| tree | 7c38566d586b22626a7a49ebdcfd0e6c3767974a /kernel/vmbytecodes.ml | |
| parent | 33e748514dad9459885006a1523d107d556be22b (diff) | |
[search] Don't use ad-hoc Dumpglob table for Search
This is an alternative to #12663 ; much preferable as the kind
information is already stored in the constant object.
Diffstat (limited to 'kernel/vmbytecodes.ml')
0 files changed, 0 insertions, 0 deletions