From 2528533d7877ecf99d880650e1c81c78190ca25d Mon Sep 17 00:00:00 2001
From: Paul Steckler <steck@stecksoft.com>
Date: Fri, 19 Jan 2018 16:43:14 -0500
Subject: update location on tab switch, issue 6624

---
 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 f06a48aeb..99ff763e2 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -56,6 +56,7 @@ val insert_xml : ?mark:GText.mark -> ?tags:GText.tag list ->
   #GText.buffer_skel -> Richpp.richpp -> unit
 
 val set_location : (string -> unit) ref
+val display_location : GText.iter -> unit
 
 (* In win32, when a command-line is to be executed via cmd.exe
    (i.e. Sys.command, Unix.open_process, ...), it cannot contain several
@@ -95,4 +96,3 @@ val io_read_all : Glib.Io.channel -> string
 
 val run_command :
   (string -> unit) -> (Unix.process_status -> unit) -> string -> unit
-
-- 
cgit v1.2.3