aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/utils/configwin_ihm.mli
Commit message (Collapse)AuthorAge
* Removing dead code in CoqIDE.Gravatar Pierre-Marie Pédrot2016-09-21
There was a pile of dead code inherited from Cameleon just sitting around and not used at all. This code was introduced in 2003 and never actually used.