Revision bd7123a411e56fdbd771174a8f514d7766ace506

Committed on 26/04/2013 7:10 am by Gaetano Giunta <gg@ez.no> [GitHub Diff]

Remove unused options from config file