Merge pull request #2816 from flaviut/optionals-to-options

Rename optionals module to options
This commit is contained in:
Andreas Rumpf
2015-05-26 22:50:35 +02:00