Revision 75b43d58e4d3db92d3d53b44f067143432093f3e

Committed on 22/05/2017 7:14 am by Jérôme Vieilledent <[email protected]> [GitHub Diff]

Merge branch '1.0'