diff --git a/docbuild-8.sh b/docbuild-8.sh index f854fdfad0..4c7b738788 100755 --- a/docbuild-8.sh +++ b/docbuild-8.sh @@ -1,6 +1,18 @@ #!/bin/sh -PATH=~/asciidoc/bin:$PATH \ -make prefix=/var/tmp/asciidoc8 \ - WEBDOC_DEST=/var/tmp/asciidoc8/webdoc \ +case "$1" in +7) + V=7 + EXTRA= + ;; +8 | '') + V=8 + PATH=~/asciidoc/bin:$PATH + EXTRA=ASCIIDOC8=YesPlease + ;; +esac + +make prefix=/var/tmp/asciidoc$V \ + WEBDOC_DEST=/var/tmp/asciidoc$V/webdoc \ + $EXTRA \ install install-webdoc