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

[David]

Revision: demexp--cduce--0.3--patch-30
Archive: address@hidden
Creator: David MENTRE <address@hidden>
Date: Wed Feb 16 22:24:23 CET 2005
Standard-date: 2005-02-16 21:24:23 GMT
New-files: lib/.arch-ids/.arch-inventory.id
    lib/.arch-ids/perf.ml.nw.id lib/.arch-inventory
    lib/perf.ml.nw
Modified-files: Makefile config.ml
    srv/demexp-server-book.tex
New-patches: address@hidden/demexp--cduce--0.3--patch-30
Summary: new module Perf to provide time measurement support
Keywords: lib, server

* lib/Perf: new module that provides functions to manipulate timers, to
  store their results and get statistics.

* Makefile
  srv/demexp-server-book.tex: include it in server.