aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/pp.ml
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-04-23 14:55:11 +0200
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-04-23 16:02:45 +0200
commit16d301bab5b7dec53be4786b3b6815bca54ae539 (patch)
treec595fc1fafd00a08cb91e53002610df867cf5eed /lib/pp.ml
parent915c8f15965fe8e7ee9d02a663fd890ef80539ad (diff)
Remove almost all the uses of string concatenation when building error messages.
Since error messages are ultimately passed to Format, which has its own buffers for concatenating strings, using concatenation for preparing error messages just doubles the workload and increases memory pressure.
Diffstat (limited to 'lib/pp.ml')
-rw-r--r--lib/pp.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/pp.ml b/lib/pp.ml
index d672f06db..9667f7270 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -249,7 +249,7 @@ let escape_string s =
else escape_at s (i-1) in
escape_at s (String.length s - 1)
-let qstring s = str ("\""^escape_string s^"\"")
+let qstring s = str "\"" ++ str (escape_string s) ++ str "\""
let qs = qstring
let quote s = h 0 (str "\"" ++ s ++ str "\"")