aboutsummaryrefslogtreecommitdiff
path: root/ide/configwin_ihm.ml
AgeCommit message (Expand)Author
2018-12-09[doc] Enable Warning 50 [incorrect doc comment] and fix comments.Emilio Jesus Gallego Arias
2018-11-11A private copy of lablgtk's question_box supporting the "parent" option.Hugo Herbelin
2018-11-11CoqIDE: ensure that the configuration box is not hidden by the main window.Hugo Herbelin
2018-05-24[ide] Move common protocol library to its own folder/object.Emilio Jesus Gallego Arias