diff options
Diffstat (limited to 'jjb/doctor/docu-verify.sh')
| -rwxr-xr-x[-rw-r--r--] | jjb/doctor/docu-verify.sh | 28 |
1 files changed, 1 insertions, 27 deletions
diff --git a/jjb/doctor/docu-verify.sh b/jjb/doctor/docu-verify.sh index f337a7fae..72d02cfe2 100644..100755 --- a/jjb/doctor/docu-verify.sh +++ b/jjb/doctor/docu-verify.sh @@ -2,32 +2,6 @@ set -e set -o pipefail -project="$(git remote -v | head -n1 | awk '{{print $2}}' | sed -e 's,.*:\(.*/\)\?,,' -e 's/\.git$//')" export PATH=$PATH:/usr/local/bin/ -git_sha1="$(git rev-parse HEAD)" -docu_build_date="$(date)" - -files=() -while read -r -d ''; do - files+=("$REPLY") -done < <(find * -type f -iname '*.rst' -print0) - -for file in "${{files[@]}}"; do - - file_cut="${{file%.*}}" - gs_cp_folder="${{file_cut}}" - - # sed part - sed -i "s/_sha1_/$git_sha1/g" $file - sed -i "s/_date_/$docu_build_date/g" $file - - # rst2html part - echo "rst2html $file" - rst2html $file > $file_cut".html" - - echo "rst2pdf $file" - rst2pdf $file -o $file_cut".pdf" - -done - +make |