Git Developer Pages

This is a tentative homepage for information on Git development. If you stumbled into this by mistake, you may want:

These pages are intended to collect information useful to Git developers, including collaborative editing of documents (i.e., it is an alternative to us having a wiki, but one that is edited entirely via git pushes).

Note that this page is an experiment and a work in progress. It may go away at any time if it turns out not to be useful.