log Docs/options.md @ 738:eae54468321b

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