diff options
| author | letouzey | 2011-09-05 16:46:50 +0000 |
|---|---|---|
| committer | letouzey | 2011-09-05 16:46:50 +0000 |
| commit | e4c505927b0ebe06f87ecc14567431822e8e0b5c (patch) | |
| tree | b466d6987134703e2e5e87ad2c6ed6e7bd628455 /plugins | |
| parent | bdf8b4edb650c847f83d520d31f23f14c58233b6 (diff) | |
Util.error now creates UserError(_,msg) instead of UserError(str,str)
This only affects display of errors when flag -debug is used,
and it avoids strange message like "Error: in msg: msg"
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14450 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions