aboutsummaryrefslogtreecommitdiff
path: root/lib/pp.ml
diff options
context:
space:
mode:
authorGuillaume Melquiond2015-04-23 14:55:11 +0200
committerGuillaume Melquiond2015-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 d672f06dbb..9667f7270e 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 "\"")