summaryrefslogtreecommitdiff
path: root/src/manager.ml
diff options
context:
space:
mode:
authorAlex AUVOLAT <alex.auvolat@ens.fr>2014-05-25 22:38:39 +0200
committerAlex AUVOLAT <alex.auvolat@ens.fr>2014-05-25 22:38:39 +0200
commitaefaa158e36cd65afa98d6b7c3f0a3d0717e13a4 (patch)
tree70b10cd5e81c385dd5979ac8f338506b38f6e0f0 /src/manager.ml
parent0140792c8111d2dd1cf9004f2e3e602ec34ed30a (diff)
downloadSystemeReseaux-Projet-aefaa158e36cd65afa98d6b7c3f0a3d0717e13a4.tar.gz
SystemeReseaux-Projet-aefaa158e36cd65afa98d6b7c3f0a3d0717e13a4.zip
Simplify protocols & stuff
Diffstat (limited to 'src/manager.ml')
-rw-r--r--src/manager.ml10
1 files changed, 5 insertions, 5 deletions
diff --git a/src/manager.ml b/src/manager.ml
index 1e6a0df..9498d8c 100644
--- a/src/manager.ml
+++ b/src/manager.ml
@@ -21,7 +21,7 @@ let pool_count = ref 0
(* Server data structures *)
type task_el =
- | Task of task_descr * bool
+ | Task of task_descr
| MsgTask of string * msg_task_descr
type client_status =
@@ -82,7 +82,7 @@ let push_task server task =
c.send
(match task with
| MsgTask(a, b) -> GiveMsgTask(a, b)
- | Task(a, b) -> GiveTask(a, b))
+ | Task(a) -> GiveTask(a))
let get_task server =
Queue.pop server.tasks
@@ -172,7 +172,7 @@ let rec server_run server =
cli.status <- Waiting
else cli.send (match Queue.pop server.tasks with
| MsgTask(a, b) -> GiveMsgTask(a, b)
- | Task(a, b) -> GiveTask(a,b))
+ | Task(a) -> GiveTask(a))
| Some r ->
cli.send(FinalResult r);
client_disconnect server cli
@@ -197,9 +197,9 @@ let rec server_run server =
c.send(FinalResult x);
client_disconnect server c)
!p
- | GiveTask(a, b) ->
+ | GiveTask(a) ->
dbg "got Task";
- push_task server (Task(a, b))
+ push_task server (Task(a))
| GiveMsgTask(a, b) ->
dbg "got MsgTask";
push_task server (MsgTask(a, b))