diff options
| author | Pierre-Marie Pédrot | 2019-04-29 14:43:42 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-04-29 14:43:42 +0200 |
| commit | deb962b17448e22ba00cba24d2e77654b8406041 (patch) | |
| tree | 9715dd8f80387b30a876ee5b2f903a77a3eec138 /dev | |
| parent | f08dacb28213f7da273d6594b317848dd5d776a8 (diff) | |
| parent | 8edf5a8e278f0bfa60207fe825a6d993e5be6ec2 (diff) | |
Merge PR #10014: CoqIDE: load coqiderc after coqide.keys
Reviewed-by: ppedrot
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions