diff options
| author | Hugo Herbelin | 2015-07-03 21:13:05 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-08-02 19:13:51 +0200 |
| commit | 21525bae8801d98ff2f1b52217d7603505ada2d2 (patch) | |
| tree | c456d9401d98198d30bca1b2c6df5390b858f893 /kernel | |
| parent | b78d86d50727af61e0c4417cf2ef12cbfc73239d (diff) | |
Cosmetic in evarconv.ml: naming a local function for better readibility.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions