The DDD preferences are saved in a file called “.ddd/init” in your home directory. Locate that file and move it away to a safe place. This will reset your settings to the default. As an advanced user, you can also edit the file and delete lines related to fonts. The DDD manual lists all the resources you can set using this file.
Cheers,
Andreas (the one who built this into DDD author some 16 years ago)
On 09.05.2016, at 14:37, Johan Smit <address@hidden> wrote:Hi,I tried to get the ddd font smaller, and must have made a mistake. Now the font is so big, I cannot do anything.DDD is installed on a Raspberry Pi running Jessie (Raspbian 8).I tried the find command, but I cannot find the files or directory ddd is installed on. My knowledge of Linux is not the best, and I cannot find the parameters needed for the find command.I tried removing and re-installing DDD, and the result is still the same.Any help will be much appreciated.Thank youJohan Smit
|
|
Andreas Zeller |
Professor | Saarland University www.st.cs.uni-saarland.de/zeller | @AndreasZeller address@hidden | +49 681 302-70970 |
