diff options
| author | Maxime Dénès | 2018-04-20 17:17:04 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-04-20 17:17:04 +0200 |
| commit | 239e28f71192d7537bc6ea283c806ba28fa1c016 (patch) | |
| tree | 66332e6670c648a73284bc97ed36b6174a8002f6 /kernel/kernel.mllib | |
| parent | 350ee43d73ee4d6c9b6c3fd24cae3aca8a2b5ce4 (diff) | |
| parent | 93c8e14d0c9bc233b2dcf213485b62a533b34580 (diff) | |
Merge PR #6908: Move VM global tables from C to ML
Diffstat (limited to 'kernel/kernel.mllib')
| -rw-r--r-- | kernel/kernel.mllib | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index 370185a721..5d270125a4 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -43,6 +43,6 @@ Subtyping Mod_typing Nativelibrary Safe_typing -Vm Csymtable +Vm Vconv |