check for a "git push" having updated the issue db, and reload if so

Details

2008-11-06 04:20 GMT	William Morgan <wmorgan-ditz@...>	commented
maybe once issue 738933ad: comments should be in separate files, like issues are is done, it will make sense to revisit this.

2008-11-06 01:43 GMT	William Morgan <wmorgan-ditz@...>	closed with disposition wontfix
it's possible to get conflicts (multiple people commenting on the same issue comes to mind), so it's going to have to be a manual process for now.

2008-11-01 21:52 GMT	William Morgan <wmorgan-ditz@...>	commented
actually it's a little more complicated than that, because the working directory doesn't get automatically updated when you push. so either sheila has to poll every once in a while, or it has to reset the working directory when differences are detected. probably the latter is the best approach because it doesn't incur any unnecessary network traffic. (submitted via Sheila by 68.127.146.40 ())

2008-11-01 20:32 GMT	William Morgan <wmorgan-ditz@...>	created