summaryrefslogtreecommitdiff
path: root/src/session.mli
diff options
context:
space:
mode:
Diffstat (limited to 'src/session.mli')
-rw-r--r--src/session.mli2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/session.mli b/src/session.mli
index 5209878..9711402 100644
--- a/src/session.mli
+++ b/src/session.mli
@@ -98,3 +98,5 @@ val show_config : world -> session_data -> string list -> string
val reference_path_exists : world -> session_data -> string list -> bool
val get_path_type : ?legacy_format:bool -> world -> session_data -> string list -> string
+
+val get_completion_env : ?legacy_format:bool -> world -> session_data -> string list -> string