Revision bd7123a411e56fdbd771174a8f514d7766ace506

Committed on 26/04/2013 7:10 am by Gaetano Giunta <[email protected]> [GitHub Diff]

Remove unused options from config file