summaryrefslogtreecommitdiff
path: root/ide/utils
ModeNameSize
-rw-r--r--configwin.ml3265logplain
-rw-r--r--configwin.mli13836logplain
-rw-r--r--configwin_html_config.ml3339logplain
-rw-r--r--configwin_ihm.ml42984logplain
-rw-r--r--configwin_keys.ml115733logplain
-rw-r--r--configwin_messages.ml2350logplain
-rw-r--r--configwin_types.ml11764logplain
-rw-r--r--editable_cells.ml3557logplain
-rw-r--r--okey.ml5525logplain
-rw-r--r--okey.mli4943logplain
-rw-r--r--uoptions.ml22246logplain
-rw-r--r--uoptions.mli6206logplain