diff options
| author | Hugo Herbelin | 2021-04-02 19:19:48 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2021-04-18 19:18:45 +0200 |
| commit | 32cc7cb03f879d089e226958ab8e89cbcde79d10 (patch) | |
| tree | 26d82a9ee92b968e0491ea6366681017b2bf7e57 /dev/header.c | |
| parent | 3167c19fbca224c4d88665ef47dedbd483671f84 (diff) | |
Coqide: on MacOS X, allow the command key to be set/unset as a modifier.
This is done by:
- allowing the <Meta> gtk modifier (gtk internal name for Command) to
be used as a modifier by default on MacOS X
- printing it <cmd> in the preference window when on MacOS X
Diffstat (limited to 'dev/header.c')
0 files changed, 0 insertions, 0 deletions