Merge pull request #1423 from chandnich/sgi-575/dyncfg
authorDimitris Papastamos <[email protected]>
Wed, 20 Jun 2018 08:50:56 +0000 (09:50 +0100)
committerGitHub <[email protected]>
Wed, 20 Jun 2018 08:50:56 +0000 (09:50 +0100)
Sgi 575/dyncfg


Trivial merge