Add a edit in github button to documentation

[BoPeng]

It is useful for people with write permission to edit our documentation, although a hook is needed to generate HTML pages from MD ones.