aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-03-05 10:27:51 +0100
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-03-05 11:59:46 +0100
commit9b4849d9d2271f91a6e32675d792a68951cbc2b6 (patch)
tree5ad46162ca68a0bf0024ecd748ed0ec2ef903ee0 /doc/refman
parent780996250ba3fd4d36ad06fefe319eb69fe919b0 (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