aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/utils
ModeNameSize
-rw-r--r--config_file.ml28991logplain
-rw-r--r--config_file.mli15221logplain
-rw-r--r--configwin.ml3666logplain
-rw-r--r--configwin.mli14185logplain
-rw-r--r--configwin_ihm.ml44702logplain
-rw-r--r--configwin_keys.ml115904logplain
-rw-r--r--configwin_messages.ml2575logplain
-rw-r--r--configwin_types.ml11888logplain
-rw-r--r--editable_cells.ml3501logplain
-rw-r--r--okey.ml5462logplain
-rw-r--r--okey.mli5136logplain