diff options
| author | Thomas Schwinge <tschwinge@gnu.org> | 2008-11-23 00:57:41 +0100 |
|---|---|---|
| committer | Thomas Schwinge <tschwinge@gnu.org> | 2008-11-23 00:57:41 +0100 |
| commit | 9e7a5b8a0628331aaf9737cd8825093d2a2a43cc (patch) | |
| tree | 6472b33bf68c2081a0ca265b0dd365d1e62cb900 /microkernel | |
| parent | 59d93ca765b359644d562f24f158f7e287678cb4 (diff) | |
When creating the official pages, use ``--no-usedirs'', so that not too many
separate directories have to be created.
Diffstat (limited to 'microkernel')
0 files changed, 0 insertions, 0 deletions