run make on previous merge

diff --git a/docs/assets/css/bootstrap.css b/docs/assets/css/bootstrap.css
index 0160bf1f63b51510d6d8460ca773b4f45f5d5a07..cf42c13e5274c8d6a1b1564b86b55bf463764e60 100644 (file)
--- a/docs/assets/css/bootstrap.css
+++ b/docs/assets/css/bootstrap.css
@@ -3867,7 +3867,8 @@ input[type="submit"].btn.btn-mini {
   background-color: #0088cc;
 }
 
-.nav-list [class^="icon-"] {
+.nav-list [class^="icon-"],
+.nav-list [class*=" icon-"] {
   margin-right: 2px;
 }