diff options
| author | Emilio Jesus Gallego Arias | 2016-10-10 17:10:23 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-02-14 23:29:56 +0100 |
| commit | 2a4f21db56400ee8928f33c3b47edfee54579afc (patch) | |
| tree | fdd7e3e063cc6b9a005db818856b8b457c567e5b /kernel/type_errors.ml | |
| parent | 0ca1717a3a1243d3fd905bb2f6c3d427f1f98dc6 (diff) | |
[safe-string] Use `String.init` to build string.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions