Revision 1de023f5298b4be5506f474ba06afe71225dfe28

Committed on 05/11/2013 2:59 pm by Gaetano Giunta <giunta.gaetano@gmail.com> [GitHub Diff]

Fixes; allow version number on command line