diff options
author | Alexey Neyman <stilor@att.net> | 2018-04-11 04:27:07 (GMT) |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-04-11 04:27:07 (GMT) |
commit | ffc638142d8bb5d70204047a7bd3bdd34b127d85 (patch) | |
tree | 317cf27c6163d608a3df30e15eecc540c7020ef4 /maintainer/download-docs.sh | |
parent | 7c3422675909ea8b117f94a26170af06a265477e (diff) | |
parent | c4608f07f7e06a58d48d74b64296be663a94c604 (diff) |
Merge pull request #937 from stilor/build-autotoolize
Autotoolize crosstool-ng
Diffstat (limited to 'maintainer/download-docs.sh')
-rwxr-xr-x | maintainer/download-docs.sh | 59 |
1 files changed, 59 insertions, 0 deletions
diff --git a/maintainer/download-docs.sh b/maintainer/download-docs.sh new file mode 100755 index 0000000..3514a57 --- /dev/null +++ b/maintainer/download-docs.sh @@ -0,0 +1,59 @@ +#!/bin/bash + +# Usage: +# download-docs.sh TOP-LEVEL-DIR MANUAL-FILES... +distdir=${1} +shift + +# Configurable portions +docs_git=https://github.com/crosstool-ng/crosstool-ng.github.io.git +docs_subdir=_pages/docs + +# Clone a repository for docs. Github does not support 'git archive --remote='. +set -ex +git clone --depth=1 "${docs_git}" "${distdir}/site-docs" + +# Copy the docs instead of the MANUAL_ONLINE placeholder +mkdir -p "${distdir}/docs/manual" +while [ -n "${1}" ]; do + case "${1}" in + docs/manual/*) ;; + *) echo "Expected file not in docs/manual/: $1" >&2; exit 1;; + esac + input="${distdir}/site-docs/${docs_subdir}/${1#docs/manual/}" + if [ ! -r "${input}" ]; then + echo "Not found: ${1}" >&2 + exit 1 + fi + awk ' +BEGIN { skip=0; } + { + if ($0=="---") { + if (NR==1) { + skip=1 + next + } + else if (skip) { + skip=0 + next + } + } + if (!skip) { + print $0 + } + } + ' < "${input}" > "${distdir}/${1}" + rm -f "${input}" + shift +done +extra_md_pages=false +for i in "${distdir}/site-docs/${docs_subdir}/"*.md; do + if [ -r "${i}" ]; then + echo "Unpackaged page in the manual: ${i#${distdir}/site-docs/${docs_subdir}/}" + extra_md_files=true + fi +done +if [ "${extra_md_files}" = "true" ]; then + exit 1 +fi +rm -rf "${distdir}/site-docs" |