summaryrefslogtreecommitdiff
path: root/src/session.mli
diff options
context:
space:
mode:
Diffstat (limited to 'src/session.mli')
-rw-r--r--src/session.mli5
1 files changed, 3 insertions, 2 deletions
diff --git a/src/session.mli b/src/session.mli
index 4bae311..f7469e0 100644
--- a/src/session.mli
+++ b/src/session.mli
@@ -15,12 +15,13 @@ type session_data = {
conf_mode: bool;
changeset: cfg_op list;
client_app: string;
- user: string
+ user: string;
+ client_pid: int32
}
exception Session_error of string
-val make : world -> string -> string -> session_data
+val make : world -> string -> string -> int32 -> session_data
val set_modified : session_data -> session_data