Merge "addendum to prior change for github compatibility"
authorEric Z <ezavesky@research.att.com>
Thu, 12 Jul 2018 19:06:23 +0000 (19:06 +0000)
committerGerrit Code Review <gerrit@acumos.org>
Thu, 12 Jul 2018 19:06:23 +0000 (19:06 +0000)

Trivial merge