log Docs/options.md @ 739:4073582a2911

age author description
Mon, 05 Aug 2019 13:19:31 +0200 David Demelier vanilla: consolidate options with lint-options.sh
Fri, 02 Aug 2019 21:20:00 +0200 David Demelier vanilla: update documentation