diff options
| author |  Cyprien Mangin <cyprien.mangin@m4x.org> | 2016-06-02 11:34:10 +0200 |
|---|---|---|
| committer | Cyprien Mangin <cyprien.mangin@m4x.org> | 2016-06-02 11:34:10 +0200 |
| commit | abd469790c2e144f693e1b21c5cdc03aee178e6d (patch) | |
| tree | 7cbcbd2fdce7cab65a3d045da045ea2e21cd510d /ide/preferences.mli | |
| parent | 2911de377786ad525dd9407968dae7c1973d7190 (diff) | |
Merge the user queries tab with the shortcut tab.
Diffstat (limited to 'ide/preferences.mli')
0 files changed, 0 insertions, 0 deletions