diff options
| author | Maxime Dénès | 2016-07-08 14:50:32 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-07-08 14:50:32 +0200 |
| commit | 78063b84f46de33de8ad58f80e45a90fa290dcd6 (patch) | |
| tree | 3816bf19f932eab1cadce00c0448d6f6822cde7c /kernel/nativecode.ml | |
| parent | e1661dc9a43b34526437e9bc3029e6320e09f899 (diff) | |
Add a few fixes in CHANGES that were forgotten.
We should really automate the generation of the log of fixes for CHANGES.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions