diff options
| author | Pierre-Marie Pédrot | 2019-02-04 13:19:34 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-02-04 13:19:34 +0100 |
| commit | 127f1fe146264a87d7a8cb04ab8ea34201b5c93a (patch) | |
| tree | 941b44ef3191544916f587de76f574d91545a7cb /kernel/vm.ml | |
| parent | 129d47518ae950c6ef1b69763e93cd70c14863f6 (diff) | |
| parent | 25aaa4c5e9da90af41629d574dbc905f3781acd2 (diff) | |
Merge PR #9368: Discard argument names of section variables on section close
Reviewed-by: gares
Reviewed-by: ppedrot
Diffstat (limited to 'kernel/vm.ml')
0 files changed, 0 insertions, 0 deletions