| commit | 6bc55c435ac398a4a6bc5c21e4b85a1bfd289a54 | [log] [tgz] |
|---|---|---|
| author | Jack Jansen <jack.jansen@cwi.nl> | Wed Oct 24 08:49:59 2001 +0000 |
| committer | Jack Jansen <jack.jansen@cwi.nl> | Wed Oct 24 08:49:59 2001 +0000 |
| tree | a9c73d79f70c1d1db81250e3e11432eb75afa1e6 | |
| parent | 72af01aac6ccf6b7b3407e0e6c5f4e11ff101d92 [diff] |
Oops, undo previous change, which wasn't supposed to escape from my machine. Luckily everyone is asleep, so I didn't have to use the time machine.