diff options
| author |  Joey Hess <joey@kitenet.net> | 2012-11-08 16:44:23 -0400 |
|---|---|---|
| committer | Joey Hess <joey@kitenet.net> | 2012-11-08 16:46:29 -0400 |
| commit | f9bf6fbcb9ef2d4afc51b60387d58db6b5cb401a (patch) | |
| tree | 68a08e40f572520c24814d7bacc4271aca32b1dd /Git.hs | |
| parent | e146cc372b8daa70fa093c9f27cedf7188ce72fc (diff) | |
xmpp push control flow
It might even work, although nothing yet triggers XMPP pushes.
Also added a set of deferred push messages. Only one push can run at a
time, and unrelated push messages get deferred. The set will never grow
very large, because it only puts two types of messages in there, that
can only vary in the client doing the push.
Diffstat (limited to 'Git.hs')
0 files changed, 0 insertions, 0 deletions