make customized setting of plugin_dir work in bootstrap mode
[tools/mic.git] / etc /
2012-12-20 Gui Chenupdate documentation
2012-12-19 Gui ChenMerge branch 'release-0.15' into devel
2012-09-26 Gui Chenrelocate dist files and add change log