[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Demexp-cvs] arch commit: demexp--cduce--0.3--patch-44
From: |
David |
Subject: |
[Demexp-cvs] arch commit: demexp--cduce--0.3--patch-44 |
Date: |
Sun, 06 Mar 2005 16:33:47 +0100 |
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.
[Prev in Thread] |
Current Thread |
[Next in Thread] |
- [Demexp-cvs] arch commit: demexp--cduce--0.3--patch-44,
David <=