use docs_menu as the default menu style for the whole website
[web.git] / README
2016-03-31 John Crispinadd README file