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

[David]

Revision: demexp--cduce--0.3--patch-32
Archive: address@hidden
Creator: David MENTRE <address@hidden>
Date: Sun Feb 20 19:26:16 CET 2005
Standard-date: 2005-02-20 18:26:16 GMT
Modified-files: Makefile lablgtk2-clnt/browser.ml.nw
    lablgtk2-clnt/demexp-lablgtk2-client-book.tex
    lablgtk2-clnt/demexp-lablgtk2-client.ml.nw
    lib/perf.ml.nw srv/demexp-server-book.tex
New-patches: address@hidden/demexp--cduce--0.3--patch-32
Summary: performance measurement in client
Keywords: client

* Makefile: compile client with lib/Perf module.

* lablgtk2-clnt/Browser: add some timers.

* lablgtk2-clnt/demexp-lablgtk2-client.ml.nw: print timer results on
  exit.

* lib/Perf: improve formatting of printed timers. New function
  "print_timers" to display timer on standard output.

* srv/demexp-server-book.tex,
  lablgtk2-clnt/demexp-lablgtk2-client-book.tex: update to do lists.