aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/utils
ModeNameSize
-rw-r--r--configwin.ml2806logplain
-rw-r--r--configwin.mli8113logplain
-rw-r--r--configwin_ihm.ml25128logplain
-rw-r--r--configwin_ihm.mli3490logplain
-rw-r--r--configwin_messages.ml2575logplain
-rw-r--r--configwin_types.mli6486logplain