diff options
| author | Guillaume Melquiond | 2015-03-05 10:27:51 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2015-03-05 11:59:46 +0100 |
| commit | 9b4849d9d2271f91a6e32675d792a68951cbc2b6 (patch) | |
| tree | 5ad46162ca68a0bf0024ecd748ed0ec2ef903ee0 /kernel/nativelambda.ml | |
| parent | 780996250ba3fd4d36ad06fefe319eb69fe919b0 (diff) | |
Do not prepend a "Error:" header when the error is expected by the user.
This commit also removes the extraneous "=>" token from Fail messages and
prevents them from losing all the formatting information.
Diffstat (limited to 'kernel/nativelambda.ml')
0 files changed, 0 insertions, 0 deletions