Pushed the patches to master and rel_3_0, along with a further patch that makes a whitespace change to quiet a -Wmisleading-indentation warning. Thanks, Chris and Jason!
Pushed the patches to master and rel_3_0, along with a further patch that makes a whitespace change to quiet a -Wmisleading- indentation warning. Thanks, Chris and Jason!