diff options
| author | Pierre-Marie Pédrot | 2021-04-19 19:06:18 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-04-19 19:06:18 +0200 |
| commit | d89f5c935af6e6055691b9980c7dfdfa481b6c4f (patch) | |
| tree | ad9da0bb302c58b5f015ef104447579ac8fb711f /dev/ci | |
| parent | b53642ec813178fedd3e646832e7c033b8163f52 (diff) | |
| parent | 32cc7cb03f879d089e226958ab8e89cbcde79d10 (diff) | |
Merge PR #14060: Coqide: on MacOS X, allow the command (⌘) key to be set/unset as a modifier
Reviewed-by: ppedrot
Diffstat (limited to 'dev/ci')
0 files changed, 0 insertions, 0 deletions