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

[David]

Revision: demexp--cduce--0.3--patch-12
Archive: address@hidden
Creator: David MENTRE <address@hidden>
Date: Mon Feb  7 22:08:00 CET 2005
Standard-date: 2005-02-07 21:08:00 GMT
New-files: scripts/.arch-ids/=id
    scripts/.arch-ids/launch-demexp.id
    scripts/launch-demexp
New-directories: scripts scripts/.arch-ids
Modified-files: config.ml
New-patches: address@hidden/demexp--cduce--0.3--patch-12
Summary: script to re-launch the bytecode server on failure
Keywords: server

* scripts/launch-demexp: a shell script that starts the bytecode demexp
  server and re-launches in case of failure, up to a 20 times.

* config.ml: bump up server and client version number.