diff options
author | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-03-05 10:27:51 +0100 |
---|---|---|
committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-03-05 11:59:46 +0100 |
commit | 9b4849d9d2271f91a6e32675d792a68951cbc2b6 (patch) | |
tree | 5ad46162ca68a0bf0024ecd748ed0ec2ef903ee0 /doc/refman | |
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 'doc/refman')
0 files changed, 0 insertions, 0 deletions