From 4bad8c9a03075faf3ba63e35648339650621e4b5 Mon Sep 17 00:00:00 2001
From: Olivier Blanvillain <olivier.blanvillain@gmail.com>
Date: Tue, 26 Sep 2017 15:35:17 +0200
Subject: [PATCH] Add chat widget in the dotty website

Inspired from the cats documentation

The button color is changed to gray to make it less intrusive
---
 doc-tool/resources/_layouts/main.html | 7 +++++++
 doc-tool/resources/css/dottydoc.css   | 4 ++++
 2 files changed, 11 insertions(+)

diff --git a/doc-tool/resources/_layouts/main.html b/doc-tool/resources/_layouts/main.html
index 364da6fb7ade..137d517f1bbf 100644
--- a/doc-tool/resources/_layouts/main.html
+++ b/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>
diff --git a/doc-tool/resources/css/dottydoc.css b/doc-tool/resources/css/dottydoc.css
index 46055f35bc34..350559355141 100644
--- a/doc-tool/resources/css/dottydoc.css
+++ b/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;
+}