rename InvariMint dir to invarimint

chubbymaggie / synoptic

Automatically exported from code.google.com/p/synoptic

0 stars 0 forks source link

rename InvariMint dir to invarimint #287

Open GoogleCodeExporter opened 9 years ago

GoogleCodeExporter commented 9 years ago

This is a minor task, but name conformity is important. Note that this will 
break the top-level build.xml file, invarimint.sh, and some other dependent 
scripts.

Original issue reported on code.google.com by bestchai on 20 Feb 2013 at 8:00