From 47fe09d27c1c47e7eed7fafc2771d5b86b507aa2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Pottier?= <francois.pottier@inria.fr>
Date: Mon, 23 Nov 2015 13:54:36 +0100
Subject: [PATCH] Improve [compare.sh] to separate stderr and stdout logs.

---
 src/compare.sh | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/src/compare.sh b/src/compare.sh
index ba341f20..cebe4bb3 100755
--- a/src/compare.sh
+++ b/src/compare.sh
@@ -27,7 +27,7 @@ sleep 1
 for FILE in "$@"
 do
   echo "Running ($FILE.mly)..."
-  { time $MENHIR --list-errors -la 2 $BASE $OPT $BENCH/$FILE.mly ; } &>$FILE.new
+  { time $MENHIR --list-errors -la 2 $BASE $OPT $BENCH/$FILE.mly ; } >$FILE.out.new 2>$FILE.err.new
 done
 
 # Try the last committed version.
@@ -38,13 +38,15 @@ sleep 1
 for FILE in "$@"
 do
  echo "Running ($FILE.mly)..."
- { time $MENHIR --list-errors -la 2 $BASE $OPT $BENCH/$FILE.mly ; } &>$FILE.old
+ { time $MENHIR --list-errors -la 2 $BASE $OPT $BENCH/$FILE.mly ; } >$FILE.out.old 2>$FILE.err.old
 done
 git stash pop
 
 # Diff.
 for FILE in "$@"
 do
-  echo "Diffing ($FILE.mly)..."
-  diff $FILE.old $FILE.new
+  echo "Diffing stderr ($FILE.mly)..."
+  diff $FILE.err.old $FILE.err.new
+  echo "Diffing stdout ($FILE.mly)..."
+  diff $FILE.out.old $FILE.out.new
 done
-- 
GitLab