Issue 2359 - Polished design of options page sidebar

skin/options.css

 /*
  * This file is part of Adblock Plus <https://adblockplus.org/>,
  * Copyright (C) 2006-2015 Eyeo GmbH
  *
  * Adblock Plus is free software: you can redistribute it and/or modify
  * it under the terms of the GNU General Public License version 3 as
  * published by the Free Software Foundation.
  *
  * Adblock Plus is distributed in the hope that it will be useful,
  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  * GNU General Public License for more details.
  *
  * You should have received a copy of the GNU General Public License
  * along with Adblock Plus.  If not, see <http://www.gnu.org/licenses/>.
  */
 
 @font-face
 {
   font-family: "Source Sans Pro";
-  src: url(fonts/SourceSansPro-Light.woff) format("woff");
+  src: url(fonts/SourceSansPro-Light.woff);
+  /* local("Ø") forces using no local font called Source Sans Pro */
+  src: local("Ø"), url(fonts/SourceSansPro-Light.woff) format("woff");
   font-weight: 300;
   font-style: normal;
 }
 
 @font-face
 {
   font-family: "Source Sans Pro";
-  src: url(fonts/SourceSansPro-Regular.woff) format("woff");
+  src: url(fonts/SourceSansPro-Regular.woff);
+  /* local("Ø") forces using no local font called Source Sans Pro */
+  src: local("Ø"), url(fonts/SourceSansPro-Regular.woff) format("woff");
   font-weight: 400;
   font-style: normal;
 }
 
 @font-face
 {
   font-family: "Source Sans Pro";
-  src: url(fonts/SourceSansPro-Semibold.woff) format("woff");
+  src: url(fonts/SourceSansPro-Semibold.woff);
+  /* local("Ø") forces using no local font called Source Sans Pro */
+  src: local("Ø"), url(fonts/SourceSansPro-Semibold.woff) format("woff");
   font-weight: 600;
   font-style: normal;
 }
 
 body
 {
   background-color: #F5F5F5;
   display: flex;
   margin: 20px 10px;
   font-family: "Source Sans Pro", sans-serif;
@@ skipping 122 matching lines @@
   border-width: 1px;
   font-weight: 600;
   -moz-border-start-color: #CDCDCD;
   -webkit-border-start-color: #CDCDCD;
   -moz-margin-end: -1px;
   -webkit-margin-end: -1px;
   -moz-margin-start: -1px;
   -webkit-margin-start: -1px;
   -moz-padding-end: 21px;
   -webkit-padding-end: 21px;
   -moz-padding-start: 21px;

[saroyanm, 2015/07/09 17:48:14]

I assume you are not using "padding: 14px 20px;" not to specify bottom and top
paddings in two places ?

[Thomas Greiner, 2015/07/10 09:48:14]

Exactly, unfortunately there's no nice way to handle this without duplication so
I chose this one for the reason you mentioned. It'd be great if we could just
do:

margin-horizontal: -1px;
padding-horizontal: 21px;

But that doesn't exist. :D

   -webkit-padding-start: 21px;
 }
 
 html[dir="rtl"] body[data-tab="general"] #tab-general,
 html[dir="rtl"] body[data-tab="advanced"] #tab-advanced,
 html[dir="rtl"] body[data-tab="help"] #tab-help
 {
   border-radius: 0px 3px 3px 0px;
 }
 
@@ skipping 698 matching lines @@
   -moz-padding-end: 10px;
   -webkit-padding-start: 0px;
   -moz-padding-start: 0px;
 }
 
 #other-language .display
 {
   -webkit-margin-start: 10px;
   -moz-margin-start: 10px;
 }