| Wed, 07 Dec 2005 15:23:22 +0100 | wenzelm | avoid unportable tail; | file | diff | annotate |
| Thu, 01 Dec 2005 22:03:06 +0100 | wenzelm | tuned; | file | diff | annotate |
| Thu, 01 Dec 2005 18:44:47 +0100 | wenzelm | cpu time = user + system; | file | diff | annotate |
| Thu, 01 Dec 2005 18:37:22 +0100 | wenzelm | timestart - setup bash environment for timing; | file | diff | annotate |