github? [Re: [Agda] Agda development]

[Jan Stolarek]

> You can merge pull requests without using the merge button on GitHub
> which avoids the message[1].
That is true. In which case it is perfectly OK to have github only as a mirror :-)

> Personally I think the message is nice, it shows the path of the commit
> history
Yes, I heard that argument and I disagree with it. Without pull requests you have linear history 
like this:

http://imageshack.us/a/img43/1091/nqu7.png

With pull requests you get obscured history that looks like this:

http://imageshack.us/a/img839/8639/u81d.png

I find it hard to see anything about commit history in the second case.

Janek