diff options
| author | Pierre Roux | 2020-09-08 10:41:03 +0200 |
|---|---|---|
| committer | Pierre Roux | 2020-09-11 22:20:28 +0200 |
| commit | 92bc869c2cec1ffb7e2d0bfcc6b64147718fbe87 (patch) | |
| tree | 89834f9ed7d88379f9284d93947b6f7d54cef1ff /interp/stdarg.mli | |
| parent | 031cc2ba1a19a06766df85b8693c72f16fa62de6 (diff) | |
Turn integer into natural in several mlgs
Negative values had no meaning there.
Those were spotted by Hugo Herbelin while reviewing #12979 .
Diffstat (limited to 'interp/stdarg.mli')
0 files changed, 0 insertions, 0 deletions