aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/utils
ModeNameSize
-rw-r--r--config_file.ml29008logplain
-rw-r--r--config_file.mli15223logplain
-rw-r--r--configwin.ml3636logplain
-rw-r--r--configwin.mli14131logplain
-rw-r--r--configwin_ihm.ml42586logplain
-rw-r--r--configwin_keys.ml115904logplain
-rw-r--r--configwin_messages.ml2581logplain
-rw-r--r--configwin_types.ml11846logplain
-rw-r--r--editable_cells.ml3512logplain
-rw-r--r--okey.ml5785logplain
-rw-r--r--okey.mli5136logplain