From 792c6f1169d63547b218d72841bdc8e8a59144c5 Mon Sep 17 00:00:00 2001
From: dotty-bot <felix.mulder@epfl.ch>
Date: Fri, 31 Mar 2017 16:08:59 +0000
Subject: Update gh-pages site for d73c8e42ca526ff2c53a17ddd1fa87044dd5bbca

---
 css/dottydoc.css | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

(limited to 'css')

diff --git a/css/dottydoc.css b/css/dottydoc.css
index 0b833830c..a89e23375 100644
--- a/css/dottydoc.css
+++ b/css/dottydoc.css
@@ -334,3 +334,23 @@ blockquote {
     color: #777;
     border-left: 0.25em solid #ddd;
 }
+
+aside {
+    padding: 15px;
+    margin: 10px 0;
+}
+
+aside.warning {
+    border-left: 3px solid #d62c2c;
+    background-color: #ffe4e4;
+}
+
+aside.notice {
+    border-left: 3px solid #4c97e4;
+    background-color: #e4ebff;
+}
+
+aside.success {
+    border-left: 3px solid #36bf1d;
+    background-color: #ebfddd;
+}
-- 
cgit v1.2.3