Eelco Dolstra 8172cd734c docdev -> devdoc ... It's "developer documentation", not "documentation developer" after all.		2016-09-01 11:07:23 +02:00
..
builder.sh	$docdev fixups: mostly to avoid empty output	2015-10-28 18:58:06 +01:00
default.nix	docdev -> devdoc	2016-09-01 11:07:23 +02:00