diff options
| author | Théo Zimmermann | 2020-12-03 10:33:33 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2020-12-03 11:33:31 +0100 |
| commit | 6a3586d80dd068c2067a8e47effed8122d0bd3b3 (patch) | |
| tree | 5ecc00b955a9d3a1492fa8d0e441fb27a7e2126a /kernel/nativelambda.mli | |
| parent | a88568e751d63d8db93450213272c8b28928dbf2 (diff) | |
[refman] Fix error names.
The @ syntax is not supported in the name, so we transform it manually
as it would have been if no name had been provided.
Diffstat (limited to 'kernel/nativelambda.mli')
0 files changed, 0 insertions, 0 deletions