diff options
| author | Maxime Dénès | 2016-09-30 10:21:00 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-09-30 10:21:00 +0200 |
| commit | e74c2e3df2ed40b6df34255f6638a93deb35f434 (patch) | |
| tree | a570e1333c65c018f119f49625da1008c4d31bdf /kernel/nativecode.ml | |
| parent | 7952c15ca3d26ae5c2807196bb7aca97bce325c6 (diff) | |
| parent | 9b1c4576d89014d686bc10f13455a52de8d793bf (diff) | |
Merge remote-tracking branch 'github/pr/294' into v8.5
Was PR#294: Make error message more helpful.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions