10 Feb
2019
10 Feb
'19
6:12 p.m.
Hi Gerd, I have attached a patch to improve the documentation of the command line. I did it some time ago and had forgotten about it, but the discussion on whether to change default options prompted me to come back to it. The change is purely to the documentation, no code changes. Please review and if it meets with your approval, commit. Thanks, Mike