aboutsummaryrefslogtreecommitdiff
path: root/config
ModeNameSize
-rw-r--r--config.mllib11logplain
-rw-r--r--coq_config.mli2577logplain
-rw-r--r--dune900logplain
-rw-r--r--list_plugins.ml232logplain