Mode | Name | Size | |
---|---|---|---|
-rw-r--r-- | configwin.ml | 3265 | logplain |
-rw-r--r-- | configwin.mli | 13836 | logplain |
-rw-r--r-- | configwin_html_config.ml | 3339 | logplain |
-rw-r--r-- | configwin_ihm.ml | 42984 | logplain |
-rw-r--r-- | configwin_keys.ml | 115733 | logplain |
-rw-r--r-- | configwin_messages.ml | 2350 | logplain |
-rw-r--r-- | configwin_types.ml | 11764 | logplain |
-rw-r--r-- | editable_cells.ml | 3557 | logplain |
-rw-r--r-- | okey.ml | 5525 | logplain |
-rw-r--r-- | okey.mli | 4943 | logplain |
-rw-r--r-- | uoptions.ml | 22246 | logplain |
-rw-r--r-- | uoptions.mli | 6206 | logplain |