Skip to content

Commit 4bad8c9

Browse files
Add chat widget in the dotty website
Inspired from the cats documentation The button color is changed to gray to make it less intrusive
1 parent 74c835d commit 4bad8c9

File tree

2 files changed

+11
-0
lines changed

2 files changed

+11
-0
lines changed

doc-tool/resources/_layouts/main.html

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -61,5 +61,12 @@
6161
}
6262
});
6363
</script>
64+
65+
<script>
66+
((window.gitter = {}).chat = {}).options = {
67+
room: 'lampepfl/dotty'
68+
};
69+
</script>
70+
<script src="https://sidecar.gitter.im/dist/sidecar.v1.js" async defer></script>
6471
</body>
6572
</html>

doc-tool/resources/css/dottydoc.css

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -270,3 +270,7 @@ aside.success {
270270
border-left: 3px solid #36bf1d;
271271
background-color: #ebfddd;
272272
}
273+
274+
.gitter-open-chat-button {
275+
background-color: gray;
276+
}

0 commit comments

Comments
 (0)