Merge pull request #292 from dyninst/wrwilliams/papercuts
authorBill Williams <wwilliam47@gmail.com>
Wed, 7 Dec 2016 21:55:02 +0000 (15:55 -0600)
committerGitHub <noreply@github.com>
Wed, 7 Dec 2016 21:55:02 +0000 (15:55 -0600)
commitc09b5ba48eb518ad6c86397e51130c566d49fa14
tree6a2b5b65616c23d59429492f485481a547e0f38e
parentae31797b354ba3e24c8a448430a91b70bdc3c1c5
parentd654b255400e34f5d518c85c97b13538516aff3a
Merge pull request #292 from dyninst/wrwilliams/papercuts

Small fixes