rename all micng to mic
[tools/mic.git] / mic / configmgr.py
2011-08-15 JF Dingrename all micng to mic