diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-05-25 14:15:53 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-05-25 14:55:53 +0200 |
| commit | c4ffe2b6725a3f8f60763228b77668aa3444f79c (patch) | |
| tree | cee051dfc74f5c7d3fbf245b31167e472fb30548 /plugins/derive/derive.ml | |
| parent | e7043eec55085f4101bfb126d8829de6f6086c5a (diff) | |
CoqIDE columns in error and job panels can be sorted.
This grants wish #4194.
Diffstat (limited to 'plugins/derive/derive.ml')
0 files changed, 0 insertions, 0 deletions