remote: do not hide the Fetch/Push/Pull button
[git-cola.git] / cola / widgets / defs.py
blobee8907606ffdcad942c21e4d743374bd42cedfe4
1 import os
2 import math
5 try:
6 scale_factor = float(os.getenv('GIT_COLA_SCALE', '1'))
7 except ValueError:
8 scale_factor = 1.0
11 def scale(value, factor=scale_factor):
12 return int(value * factor)
15 no_margin = 0
16 small_margin = scale(2)
17 margin = scale(4)
18 large_margin = scale(12)
20 no_spacing = 0
21 spacing = scale(4)
22 titlebar_spacing = scale(8)
23 button_spacing = scale(12)
25 cursor_width = scale(2)
26 handle_width = scale(4)
27 tool_button_height = scale(28)
29 default_icon = scale(16)
30 small_icon = scale(12)
31 medium_icon = scale(48)
32 large_icon = scale(96)
33 huge_icon = scale(192)
35 max_size = scale(4096)
37 border = max(1, scale(0.5))
38 checkbox = scale(12)
39 radio = scale(22)
41 logo_text = 24
43 radio_border = max(1, scale(1.0 - (1.0 / math.pi)))
45 separator = scale(3)
47 dialog_w = scale(720)
48 dialog_h = scale(445)
50 msgbox_h = scale(128)