diff options
| -rw-r--r-- | doc/buildfile | 6 | ||||
| l--------- | doc/doc.css | 1 | ||||
| l--------- | doc/intro.css | 1 | ||||
| m--------- | doc/style | 0 |
4 files changed, 4 insertions, 4 deletions
diff --git a/doc/buildfile b/doc/buildfile index 4e85906..84386da 100644 --- a/doc/buildfile +++ b/doc/buildfile @@ -10,7 +10,7 @@ css{*}: extension = css build2-toolchain-intro-a4.ps \ build2-toolchain-intro-letter.pdf \ build2-toolchain-intro-letter.ps} \ - css{common code-box pre-box intro} \ - file{a4.html2ps letter.html2ps intro.html2ps} \ - file{intro-prologue.xhtml intro-epilogue.xhtml \ + css{code-box common doc pre-box toc} \ + file{a4.html2ps letter.html2ps doc.html2ps} \ + file{doc-prologue.xhtml doc-epilogue.xhtml \ intro.cli cli.sh} diff --git a/doc/doc.css b/doc/doc.css new file mode 120000 index 0000000..6cb3fd5 --- /dev/null +++ b/doc/doc.css @@ -0,0 +1 @@ +style/doc.css
\ No newline at end of file diff --git a/doc/intro.css b/doc/intro.css deleted file mode 120000 index 71895c7..0000000 --- a/doc/intro.css +++ /dev/null @@ -1 +0,0 @@ -style/intro.css
\ No newline at end of file diff --git a/doc/style b/doc/style -Subproject 88bef7fa19d595b64944edc38696bb1ceadba2f +Subproject e8d8ccfbd637d68f6feceace9dddc5bd5c13d83 |