diff options
| -rw-r--r-- | ide/ideutils.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/ideutils.ml b/ide/ideutils.ml index 8f54175519..1464181f41 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -287,7 +287,7 @@ let stat f = Note: In a mono-thread coqide, we use the same buffer for different read operations *) -let maxread = 8192 +let maxread = 4096 let read_string = String.create maxread let read_buffer = Buffer.create maxread |