aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/utils
ModeNameSize
-rw-r--r--.cvsignore11logplain
-rw-r--r--configwin.ml2220logplain
-rw-r--r--configwin.mli12791logplain
-rw-r--r--configwin_html_config.ml2294logplain
-rw-r--r--configwin_ihm.ml41706logplain
-rw-r--r--configwin_keys.ml114688logplain
-rw-r--r--configwin_messages.ml1305logplain
-rw-r--r--configwin_types.ml10719logplain
-rw-r--r--okey.ml4480logplain
-rw-r--r--okey.mli3898logplain
-rw-r--r--uoptions.ml20461logplain
-rw-r--r--uoptions.mli4420logplain