| commit | 339ecc61f81703613d8b5536b35de3dcf745a9ad | [log] [tgz] |
|---|---|---|
| author | Jack Jansen <jack.jansen@cwi.nl> | Sun Oct 22 21:57:12 2000 +0000 |
| committer | Jack Jansen <jack.jansen@cwi.nl> | Sun Oct 22 21:57:12 2000 +0000 |
| tree | 789fa9f05454615cefceb2ad17a78eff8bd42f94 | |
| parent | 5c35f5aeee577937960ca83a775697ada32219d3 [diff] |
Updated because developer option isn't distributed separately anymore.