Simon Michael 2321c64327 doc: fix current version highlighting in web manuals		2017-01-03 11:28:30 -08:00
..
highslide	site: move manual, devguide here; move out of doc/	2015-11-05 19:32:17 -08:00
site.js	doc: fix current version highlighting in web manuals	2017-01-03 11:28:30 -08:00