diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-05-04 08:48:30 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-05-04 08:48:30 +0200 |
| commit | 9173d3b0c4127e8217e93f8aad8ccba94037b486 (patch) | |
| tree | 06da6f1a5f5b5b9d48cb9f05f8376d00fa06f521 /interp/dumpglob.ml | |
| parent | 27689bac62f85c039517cbd003f8ea74cb9b4aa7 (diff) | |
Increase the size of the dumpglob buffer for cooking notations (bug #4708).
A single terminal character can take up to 5 bytes, e.g. "''^A'".
Diffstat (limited to 'interp/dumpglob.ml')
| -rw-r--r-- | interp/dumpglob.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index 44a62ef37..85212b7ab 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -172,7 +172,7 @@ let cook_notation df sc = (* - all single quotes in terminal tokens are doubled *) (* - characters < 32 are represented by '^A, '^B, '^C, etc *) (* The output is decoded in function Index.prepare_entry of coqdoc *) - let ntn = String.make (String.length df * 3) '_' in + let ntn = String.make (String.length df * 5) '_' in let j = ref 0 in let l = String.length df - 1 in let i = ref 0 in |