Merge pull request #761 from justinsg/master
authorDan Vanderkam <danvdk@gmail.com>
Mon, 11 Jul 2016 22:20:41 +0000 (18:20 -0400)
committerGitHub <noreply@github.com>
Mon, 11 Jul 2016 22:20:41 +0000 (18:20 -0400)
Check for new options before updating synchronised graphs (Fixes #760)


Trivial merge