isa/gnome-shell
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Use points for font sizes

Browse Source 
Do a basic job of converting font sizes from pixels to points, so they
will scale will the global GNOME scale factor. Some other sizes that are
clearly related to the font sizes are changed to ems, but no comprehensive
attempt is made to get rid of px units.

https://bugzilla.gnome.org/show_bug.cgi?id=636868
This commit is contained in:
Owen W. Taylor
2011-03-04 15:54:19 -05:00
parent 971e3f679f
commit e8eec2d357
4 changed files with 38 additions and 40 deletions
Download Patch File Download Diff File Expand all files Collapse all files

4
js/ui/panel.js
View File

@ -22,8 +22,6 @@ const DateMenu = imports.ui.dateMenu;
const Main = imports.ui.main;
const Tweener = imports.ui.tweener;
const PANEL_HEIGHT = 26;
const PANEL_ICON_SIZE = 24;
const STARTUP_ANIMATION_TIME = 0.2;
@ -1044,7 +1042,7 @@ Panel.prototype = {
let primary = global.get_primary_monitor();
this.actor.set_position(primary.x, primary.y);
this.actor.set_size(primary.width, PANEL_HEIGHT);
this.actor.set_size(primary.width, -1);
this._leftCorner.relayout();
this._rightCorner.relayout();