diff options
Diffstat (limited to 'Doc')
| -rwxr-xr-x | Doc/.cvsignore | 1 | ||||
| -rwxr-xr-x | Doc/tools/push-docs.sh | 12 |
2 files changed, 12 insertions, 1 deletions
diff --git a/Doc/.cvsignore b/Doc/.cvsignore index b5159d8..8f8d035 100755 --- a/Doc/.cvsignore +++ b/Doc/.cvsignore @@ -3,3 +3,4 @@ *.zip *.tar pkglist.html +.doctype diff --git a/Doc/tools/push-docs.sh b/Doc/tools/push-docs.sh index 6dd74e2..28a4b31 100755 --- a/Doc/tools/push-docs.sh +++ b/Doc/tools/push-docs.sh @@ -26,6 +26,7 @@ else DOCTYPE="devel" fi +DOCTYPE_SPECIFIED=false EXPLANATION='' ANNOUNCE=true @@ -55,6 +56,7 @@ while [ "$#" -gt 0 ] ; do ;; -t) DOCTYPE="$2" + DOCTYPE_SPECIFIED=true shift 2 ;; -F) @@ -99,9 +101,17 @@ else exit 2 fi +# switch to .../Doc/ cd .. -# now in .../Doc/ +# If $DOCTYPE was not specified explicitly, look for .doctype in +# .../Doc/ and use the content of that file if present. +if $DOCTYPE_SPECIFIED ; then + : +elif [ -f .doctype ] ; then + DOCTYPE="`cat .doctype`" +fi + make --no-print-directory ${PKGTYPE}html || exit $? PACKAGE="html-$VERSION.$PKGEXT" scp "$PACKAGE" tools/update-docs.sh $TARGET/ || exit $? |