From 9173d3b0c4127e8217e93f8aad8ccba94037b486 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 4 May 2016 08:48:30 +0200 Subject: 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'". --- interp/dumpglob.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'interp/dumpglob.ml') 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 -- cgit v1.2.3