diff options
| author | Gaëtan Gilbert | 2018-11-17 21:07:44 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-03-14 15:46:16 +0100 |
| commit | ab8c27c589ea90ac86518cc7c1b513b740190cdc (patch) | |
| tree | aea236e67ca897ab208ae95e352b29c9d3b28a58 /kernel/type_errors.ml | |
| parent | 456919dd31f2f4bda15c6b37e4f1217bc085fc41 (diff) | |
Put [@inline] on CClosure.Mark functions
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions