diff options
| author | Adolfo Jayme Barrientos <fitojb@ubuntu.com> | 2017-08-07 04:52:45 -0500 |
|---|---|---|
| committer | Adolfo Jayme Barrientos <fitojb@ubuntu.com> | 2017-08-07 04:52:45 -0500 |
| commit | 43f159dafa3fe61c09cafc8467cdd67233a02401 (patch) | |
| tree | a3abe57e3137b61b4b85c553ae762af6873948ac /COPYING | |
| parent | 7915f35d7fca5d0720d96954beaa97c00a2c3821 (diff) | |
Rename “Basic IDE Options” to just “Basic IDE”
None of the other Options/Preferences pages have the word “Options”
in their names, because: a) it’s obvious that they’re options, and b)
having that word repeated there contravenes the macOS convention of
calling the options “preferences”.
Change-Id: I7349d20eefc50d5a92d6442a256249f64db688e7
Diffstat (limited to 'COPYING')
0 files changed, 0 insertions, 0 deletions