equal
deleted
inserted
replaced
77 path = '/' + path |
77 path = '/' + path |
78 |
78 |
79 return name, str(port), path |
79 return name, str(port), path |
80 |
80 |
81 class hgwebdir(object): |
81 class hgwebdir(object): |
82 refreshinterval = 20 |
|
83 |
|
84 def __init__(self, conf, baseui=None): |
82 def __init__(self, conf, baseui=None): |
85 self.conf = conf |
83 self.conf = conf |
86 self.baseui = baseui |
84 self.baseui = baseui |
|
85 self.ui = None |
87 self.lastrefresh = 0 |
86 self.lastrefresh = 0 |
88 self.motd = None |
87 self.motd = None |
89 self.refresh() |
88 self.refresh() |
90 |
89 |
91 def refresh(self): |
90 def refresh(self): |
92 if self.lastrefresh + self.refreshinterval > time.time(): |
91 refreshinterval = 20 |
|
92 if self.ui: |
|
93 refreshinterval = self.ui.configint('web', 'refreshinterval', |
|
94 refreshinterval) |
|
95 |
|
96 # refreshinterval <= 0 means to always refresh. |
|
97 if (refreshinterval > 0 and |
|
98 self.lastrefresh + refreshinterval > time.time()): |
93 return |
99 return |
94 |
100 |
95 if self.baseui: |
101 if self.baseui: |
96 u = self.baseui.copy() |
102 u = self.baseui.copy() |
97 else: |
103 else: |