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

[David]

Revision: demexp--dev--0.5--patch-52
Archive: address@hidden
Creator: David MENTRE <address@hidden>
Date: Sat Jul  2 14:07:00 CEST 2005
Standard-date: 2005-07-02 12:07:00 GMT
Modified-files: Announcement-0.6.txt
    srv/demexp-server.ml.nw
New-patches: address@hidden/demexp--dev--0.5--patch-52
Summary: save server pid in a file
Keywords: server

* srv/demexp-server.ml.nw: when the server starts, it saves its pid in a
  file (useful to kill it afterward).

* Announcement-0.6.txt: minor updates.