diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-08-16 00:32:23 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-08-16 03:51:20 +0200 |
| commit | 2c70dd6a256ed4cac2b74bd0c8719ab37fffcb84 (patch) | |
| tree | 4d39756908a91c73535628bbb648018799670d1b /ide/wg_Command.ml | |
| parent | 2bb05717bde540332aa814a59da3745f2097dedf (diff) | |
Simplifying CoqIDE preferences mechanism.
We use a class-based system instead of the old record-based system. This
allows for more uniformity and the possibility to define complex
interactions with preferences based on GTK signals. This will allow to
simplify some architectural choices.
Diffstat (limited to 'ide/wg_Command.ml')
0 files changed, 0 insertions, 0 deletions