Revision 1eda15d96502941d3e42592920bbd94ec3398426

Committed on 30/10/2013 2:57 pm by Gaetano Giunta <[email protected]> [GitHub Diff]

Improve task docs; remove useless task options (since any config value can now be set as option)