diff --git a/tools/build_doc.sh b/tools/build_doc.sh index 37935dd..c49a365 100755 --- a/tools/build_doc.sh +++ b/tools/build_doc.sh @@ -36,10 +36,17 @@ do exported=${i%.org}.exported exported=$(dirname $exported)/.$(basename $exported) NOW=$(date +"%m%d%H%M.%S") - extract_doc ${i} > $exported + extract_doc ${i} &> $exported + rc=$? # Make log file older than the exported files touch -t ${NOW} $exported + + # Fail if tangling failed + if [[ $rc -ne 0 ]] ; then + cat $exported + exit rc + fi done diff --git a/ci_install.sh b/tools/ci_install.sh similarity index 100% rename from ci_install.sh rename to tools/ci_install.sh diff --git a/tools/tangle.sh b/tools/tangle.sh index 7e402b6..ebd1929 100755 --- a/tools/tangle.sh +++ b/tools/tangle.sh @@ -37,10 +37,11 @@ do NOW=$(date +"%m%d%H%M.%S") tangle ${i} &> $tangled rc=$? + # Make log file older than the tangled files + touch -t ${NOW} $tangled + # Fail if tangling failed if [[ $rc -ne 0 ]] ; then cat $tangled exit rc fi - # Make log file older than the tangled files - touch -t ${NOW} $tangled done