Revision 7aebc4c5adf45e896301b4e6f152e489b04c740d

Committed on 26/02/2016 8:48 am by Gaetano Giunta <[email protected]> [GitHub Diff]

fixes for last commit