Commits on Aug 29, 2018

1. Fix bad Github merge …

   The changes in PRs #3491 and #3482 turned out to be incompatible.
   To avoind things like this, it would be ideal if PRs were not
   merged unless they were rebased and had a complete CI build first.

   

   erikd committed Aug 29, 2018
   Configuration menu

   • View commit details
   • Copy full SHA for 0092424
   • Browse repository at this point

   Copy the full SHA

   0092424 View commit details

   Browse the repository at this point in the history