chebfun/chebfun — pull request #939 by aaustin141 (2014-06-19 07:47:10+00:00)
Title: fix-prefs

Last-minute adjustments to some preference names.

This also closes #759.