diff options
| author | Emilio Jesus Gallego Arias | 2020-06-13 17:56:50 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-06-13 17:57:37 +0200 |
| commit | ce26ccfd0160265af975f84727e45bb97da39628 (patch) | |
| tree | 357c800f63cef410d480bb4d1c72f3066afe0e90 /kernel/nativecode.mli | |
| parent | 13e8d04b2f080fbc7ca169bc39e53c8dd091d279 (diff) | |
[toplevel] Annotate tailcall functions
This will ensure that we don't introduce problems as it has happened
in the past.
While we are at it, we fix one easy case of non-tail call.
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions