Bugfix: if the cache dir from the config file does not exist, do not use it

This commit is contained in:
Laurent Clouet
2015-05-01 13:24:49 +01:00
parent d74d85c174
commit 4a541a5f00

View File

@@ -242,7 +242,7 @@ public class SettingsLoader {
if (config.getNbCores() == -1 && cores != null) { if (config.getNbCores() == -1 && cores != null) {
config.setUseNbCores(Integer.valueOf(cores)); config.setUseNbCores(Integer.valueOf(cores));
} }
if (config.getUserSpecifiedACacheDir() == false && cacheDir != null) { if (config.getUserSpecifiedACacheDir() == false && cacheDir != null && new File(cacheDir).exists()) {
config.setCacheDir(new File(cacheDir)); config.setCacheDir(new File(cacheDir));
} }