diff options
author | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-04-23 14:55:11 +0200 |
---|---|---|
committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-04-23 16:02:45 +0200 |
commit | 16d301bab5b7dec53be4786b3b6815bca54ae539 (patch) | |
tree | c595fc1fafd00a08cb91e53002610df867cf5eed /lib/pp.ml | |
parent | 915c8f15965fe8e7ee9d02a663fd890ef80539ad (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.ml | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -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 "\"") |