diff options
author | Adam Chlipala <adam@chlipala.net> | 2011-07-03 12:40:00 -0400 |
---|---|---|
committer | Adam Chlipala <adam@chlipala.net> | 2011-07-03 12:40:00 -0400 |
commit | 3311911fd21e0c240788d83ff6da710dbbbc66e8 (patch) | |
tree | 57875f0e93a279eeaac3f66eac6372405cdf4b60 /src/cjr_print.sml | |
parent | dd592cc205438ef4a46f7103d0fc7113e376d358 (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.sml | 5 |
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));", |