aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/utils
ModeNameSize
-rw-r--r--.cvsignore11logplain
-rw-r--r--configwin.ml2180logplain
-rw-r--r--configwin.mli12586logplain
-rw-r--r--configwin_html_config.ml2294logplain
-rw-r--r--configwin_ihm.ml39613logplain
-rw-r--r--configwin_keys.ml114688logplain
-rw-r--r--configwin_messages.ml1305logplain
-rw-r--r--configwin_types.ml9704logplain
-rw-r--r--okey.ml4480logplain
-rw-r--r--okey.mli3898logplain
-rw-r--r--uoptions.ml20461logplain
-rw-r--r--uoptions.mli4420logplain