| commit | 0701bd64aaf5eacafa7b18f0e67273ed75943a8b | [log] [tgz] |
|---|---|---|
| author | Jack Jansen <jack.jansen@cwi.nl> | Thu Jun 03 21:55:46 2004 +0000 |
| committer | Jack Jansen <jack.jansen@cwi.nl> | Thu Jun 03 21:55:46 2004 +0000 |
| tree | 53d30e57610b5d88d073d8d56a92b51697170986 | |
| parent | 30184f3611d867124f7030dfcb182ab89245f47a [diff] |
Fix for #860242: use correct names in the "save preferences" dialog.