From 08f13d29b4b8ffbd8f967e80eeda3d40c1b26ee6 Mon Sep 17 00:00:00 2001
From: Anthony Scemama <scemama@irsamc.ups-tlse.fr>
Date: Thu, 14 Oct 2021 21:39:08 +0200
Subject: [PATCH] Cleaning tangle

---
 tools/build_doc.sh                   | 9 ++++++++-
 ci_install.sh => tools/ci_install.sh | 0
 tools/tangle.sh                      | 5 +++--
 3 files changed, 11 insertions(+), 3 deletions(-)
 rename ci_install.sh => tools/ci_install.sh (100%)

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