From 39587fe37a218ff2f975a3225ef48cc86949d809 Mon Sep 17 00:00:00 2001
From: Arnaud Giersch <arnaud.giersch@iut-bm.univ-fcomte.fr>
Date: Sat, 2 Feb 2013 15:52:03 +0100
Subject: [PATCH] Improve output of check_dist_archive.

---
 tools/check_dist_archive | 13 +++++++++++--
 1 file changed, 11 insertions(+), 2 deletions(-)

diff --git a/tools/check_dist_archive b/tools/check_dist_archive
index ca1f75e5ba..38fe76d02e 100755
--- a/tools/check_dist_archive
+++ b/tools/check_dist_archive
@@ -81,7 +81,14 @@ find b -type f \
     | sort > "$fb"
 
 diffcmd() {
-    diff -u "$fa" "$fb"
+    if cmp -s "$fa" "$fb"; then
+        status=0
+        echo "The archive looks good."
+    else
+        status=1
+        echo "Some files are missing and/or unexpected in the archive."
+        diff -u "$fa" "$fb"
+    fi
 }
 
 colordiff=$(type -p colordiff)
@@ -97,4 +104,6 @@ if [ "$interactive" = "1" ]; then
     diffcmd | colorless
 else
     diffcmd
-fi
+fi || true
+
+exit $status
-- 
2.20.1