[Demexp-cvs] arch commit: demexp--dev--0.5--patch-40

[David]

Revision: demexp--dev--0.5--patch-40
Archive: address@hidden
Creator: David MENTRE <address@hidden>
Date: Sat Jun 25 13:26:22 CEST 2005
Standard-date: 2005-06-25 11:26:22 GMT
Modified-files: srv/demexp-server.ml.nw srv/work.ml.nw
New-patches: address@hidden/demexp--dev--0.5--patch-40
Summary: handle signal on server
Keywords: server

* srv/Work: new function "schedule_server_halt" that stops the server
  after a few seconds when called. Refactor "stop_server" to use it.

* srv/demexp-server.ml.nw: setup of signal handlers on SIGINT, SIGHUP
  and SIGQUIT to stop the server when received.