On 2015-11-13 12:18, Eric Eide wrote:
Yang Chen <chenyang@cs.utah.edu> writes:I added some comments on the patch, but after that I didn't get any notifications.Maybe GitHub doesn't usually send notifications when a pull request is amendedby more commits? I don't know.
Yeah, perhaps that's the case. - Yang