[Demexp-cvs] arch commit: demexp--cduce--0.3--patch-44

[David]

Revision: demexp--cduce--0.3--patch-44
Archive: address@hidden
Creator: David MENTRE <address@hidden>
Date: Sun Mar  6 16:33:27 CET 2005
Standard-date: 2005-03-06 15:33:27 GMT
Modified-files: lablgtk2-clnt/clntflags.ml.nw
    lablgtk2-clnt/demexp-lablgtk2-client.ml.nw
    scripts/launch-demexp
New-patches: address@hidden/demexp--cduce--0.3--patch-44
Summary: new command line option --stop-server in client
Keywords: client, script

* lablgtk2-clnt/Clntflags: new flag_stop_server used by command line
  option.

* lablgtk2-clnt/demexp-lablgtk2-client.ml.nw: new command line option
  --stop-server that stops the remote server. Try to not abuse of its use!

* scripts/launch-demexp: modify launch script so that the server is not
  relaunched if it is stopped properly.