| commit | f044e090c4c8aeed0480fc56fec01e651d811680 | [log] [tgz] |
|---|---|---|
| author | Jack Jansen <jack.jansen@cwi.nl> | Thu Dec 26 22:10:53 2002 +0000 |
| committer | Jack Jansen <jack.jansen@cwi.nl> | Thu Dec 26 22:10:53 2002 +0000 |
| tree | b7e6e67606bd3aba3115bea2955f21ed61402618 | |
| parent | 9431e48d238a77422436a6b3e56a4237e87d71ea [diff] |
Changed the input field for the interpreter to use (in the preferences window) to a combobox listing the known interpreters.