Pierre Pronchery ff1cad0ef9 Rename "tools" as "doc" ... It is more appropriate given its current content.		2015-07-11 15:22:23 +02:00
..
Init	Rename "tools" as "doc"	2015-07-11 15:22:23 +02:00
project.conf	Rename "tools" as "doc"	2015-07-11 15:22:23 +02:00