When started, MMT looks for a configuration file called
mmtrc in the following order:
- a default file is included with MMT
deployfolder of the MMT repository (if MMT is run in a way that lets it find that folder)
- the user’s home folder
Later configuration entries overwrite earlier ones.
During setup a defaut configuration file is generated and placed in the
That file also includes some example configuration entries.
Configuration File Syntax
Every configuration file is split into sections introduced by
#TYPE defining the type of the following configuration entries.
Each section consists of one configuration entry per line. Each entry is a whitespace-separated list of strings.
The class for configuration entries
Its Scala doc is the primary place to document the individual entries.