summaryrefslogtreecommitdiff
path: root/src/proto.ml
diff options
context:
space:
mode:
Diffstat (limited to 'src/proto.ml')
-rw-r--r--src/proto.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/src/proto.ml b/src/proto.ml
index 1f6d8e6..df41944 100644
--- a/src/proto.ml
+++ b/src/proto.ml
@@ -4,6 +4,7 @@ open Util
type task = unit -> unit
type msg_task = string -> unit
+
type task_descr = string
type msg_task_descr = string
@@ -15,7 +16,7 @@ type message =
| Get of id * msg_task_descr
| Put of id * string
| RequestTask
- | GiveTask of task_descr * bool
+ | GiveTask of task_descr
| GiveMsgTask of string * msg_task_descr
| FinalResult of string