diff options
| author | Emilio Jesus Gallego Arias | 2018-06-10 09:45:21 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-06-10 09:45:21 +0200 |
| commit | a19746f2ff7933f0b78ecfcd78e3237ef721977a (patch) | |
| tree | 6e2bb24cac2f4d9efe589507810b2558d5cbd0d6 /kernel/nativelambda.ml | |
| parent | 51a56b1aacb516af513de64c00dd7e796f661484 (diff) | |
[lib] Fix wrong deprecation comment.
Diffstat (limited to 'kernel/nativelambda.ml')
0 files changed, 0 insertions, 0 deletions