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