diff options
| author | Felix Mulder <felix.mulder@gmail.com> | 2017-02-03 18:47:33 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-02-03 18:47:33 +0100 |
| commit | da7d7231b7f21fe1085abc569eb783590074a359 (patch) | |
| tree | 3d02c1bb742ee9f8ab860454a71e6bd93a3a806b /bin | |
| parent | b71acb9a74382742a43d82eebeff6c7602625500 (diff) | |
| parent | 96126c792562d963551132294abcb30f29f5eebd (diff) | |
| download | dotty-da7d7231b7f21fe1085abc569eb783590074a359.tar.gz dotty-da7d7231b7f21fe1085abc569eb783590074a359.tar.bz2 dotty-da7d7231b7f21fe1085abc569eb783590074a359.zip | |
Merge pull request #1939 from dotty-staging/topic/dottydoc-html-enhancements
[doc] html enhancements
Diffstat (limited to 'bin')
0 files changed, 0 insertions, 0 deletions