git tag before make dist. Check no files modified
Authored by: Jean-Francois Dockes 2014-04-29
Parent(s): [12e8ef]
Child(ren): [aef742]
