From 985e83e60b6665d17b81830aea4fce3384fe2b5a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Tue, 30 Aug 2016 20:32:13 +0200
Subject: Fix bug #5051: Large outputs are garbled.

Instead of relying on the current position of the cursor, we rather use
a dedicated mark in the message view.
---
 ide/ideutils.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'ide/ideutils.mli')

diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index 491e8e823..e32a4d9e3 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -54,7 +54,7 @@ val flash_info : ?delay:int -> string -> unit
 
 val xml_to_string : Richpp.richpp -> string
 
-val insert_xml : ?tags:GText.tag list ->
+val insert_xml : ?mark:GText.mark -> ?tags:GText.tag list ->
   #GText.buffer_skel -> Richpp.richpp -> unit
 
 val set_location : (string -> unit) ref
-- 
cgit v1.2.3