diff options
| author | Hugo Herbelin | 2020-11-10 15:14:11 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-16 13:57:15 +0100 |
| commit | eae015fa8aadab229a056eb869e2b926fa6c9dc2 (patch) | |
| tree | d005144ea8d3250b78a1de8563f58e833146ec0e /kernel/vmbytecodes.ml | |
| parent | 89a4b7e7dd82bd46db2d00b6e48b8989d3a5372b (diff) | |
Avoid exposing an internal names when "intros _ H" fails.
Diffstat (limited to 'kernel/vmbytecodes.ml')
0 files changed, 0 insertions, 0 deletions