Merge pull request #3180 from dotty-staging/chat-in-docs

Add chat widget in the docs

Author: smarter

doc-tool/resources/_layouts/main.html

@@ -61,5 +61,12 @@
                 }
             });
         </script>
+
+        <script>
+          ((window.gitter = {}).chat = {}).options = {
+            room: 'lampepfl/dotty'
+          };
+        </script>
+        <script src="https://sidecar.gitter.im/dist/sidecar.v1.js" async defer></script>
     </body>
 </html>

doc-tool/resources/css/dottydoc.css

@@ -270,3 +270,7 @@ aside.success {
     border-left: 3px solid #36bf1d;
     background-color: #ebfddd;
 }
+
+.gitter-open-chat-button {
+  background-color: gray;
+}