Merge pull request #2090 from whitequark/cxxrtl-fixes
authorwhitequark <whitequark@whitequark.org>
Tue, 26 May 2020 22:18:14 +0000 (22:18 +0000)
committerGitHub <noreply@github.com>
Tue, 26 May 2020 22:18:14 +0000 (22:18 +0000)
Minor fixes for CXXRTL


Trivial merge