prefer to use 'pbzip2'/'pgzip' than 'bzip2'/'gzip'
[tools/mic.git] / etc /
drwxr-xr-x   ..
-rw-r--r-- 5562 mic.bash
-rw-r--r-- 659 mic.conf.in