-
Simon Marlow authored
--tool is no longer a formal option: you can get the same effect by just saying tool=<tool> on the command line. This means it can also be set in a config file instead.
60a369a3
--tool is no longer a formal option: you can get the same effect by just saying tool=<tool> on the command line. This means it can also be set in a config file instead.