diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-01-22 09:41:25 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-01-22 09:41:25 +0100 |
commit | e0805eac59ee4c6c2eafae1d6b7f91530104f18f (patch) | |
tree | a36443b6a81e50986b9239f676aee2d5df5f1237 /ide/ideutils.mli | |
parent | c01b003ca1bc3bf04b538f03dadc59732d89aedc (diff) | |
parent | 2528533d7877ecf99d880650e1c81c78190ca25d (diff) |
Merge PR #6625: Update location on tab switch, issue 6624
Diffstat (limited to 'ide/ideutils.mli')
-rw-r--r-- | ide/ideutils.mli | 2 |
1 files changed, 1 insertions, 1 deletions
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 - |