Separate MPS caches for different MPS distributions based on the same MPS major version
Between MPS major versions, the MPS global caches are nicely separated (e.g. for MPS 2017.1, the cache directory is $HOME/.MPS2017.1 and for MPS 2017.2, the cache directory is $HOME/.MPS2017.2, where $HOME is your home directory, e.g. C:\Users\<yourusername> on Windows or /home/<yourusername> on Linux). Sometimes, there are reasons why you would want to change the cache … Read more