···

       
56
       
 
       
        default-result-background-corner-radius = 8;

     

       
57
       
 
       
        default-result-background-padding = "5, 10";

     

       
58
       
 
       


     

       
0
       
 
       

     

       
0
       
 
       

     

       
59
       
 
       
        clip-to-padding = false;

     

       
60
       
 
       
      };

     

       
61
       
 
       
    };

     

···

       
56
       
 
       
        default-result-background-corner-radius = 8;

     

       
57
       
 
       
        default-result-background-padding = "5, 10";

     

       
58
       
 
       


     

       
59
       
+
       
        font = lib.mkForce "Sans";

     

       
60
       
+
       


     

       
61
       
 
       
        clip-to-padding = false;

     

       
62
       
 
       
      };

     

       
63
       
 
       
    };