aboutsummaryrefslogtreecommitdiffhomepage
path: root/src/cjr_print.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2011-07-03 12:40:00 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2011-07-03 12:40:00 -0400
commit3311911fd21e0c240788d83ff6da710dbbbc66e8 (patch)
tree57875f0e93a279eeaac3f66eac6372405cdf4b60 /src/cjr_print.sml
parentdd592cc205438ef4a46f7103d0fc7113e376d358 (diff)
For non-debug builds, leave out source location info in what is shown to user
Diffstat (limited to 'src/cjr_print.sml')
-rw-r--r--src/cjr_print.sml5
1 files changed, 5 insertions, 0 deletions
diff --git a/src/cjr_print.sml b/src/cjr_print.sml
index 9b747bcb..79d7e7da 100644
--- a/src/cjr_print.sml
+++ b/src/cjr_print.sml
@@ -3112,6 +3112,11 @@ fun p_file env (ds, ps) =
NONE => box []
| SOME n => box [string "static void uw_onError(uw_context ctx, char *msg) {",
newline,
+ if Settings.getDebug () then
+ box []
+ else
+ box [string "uw_cutErrorLocation(msg);",
+ newline],
box [string "uw_write(ctx, ",
p_enamed env n,
string "(ctx, msg, 0));",