Some small changes for Dotty compatibility#757
Merged
djspiewak merged 9 commits intotypelevel:masterfrom travisbrown:topic/dotty-compatJan 27, 2020
+57-53
Commits
Commits on Jan 22, 2020
- committed
- committed
- committed
- committed
- committed
- committed
- committed
- committed
- committed
