From c8b6020bb3db38044da4f310ab6c67883a1e337f Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 31 Jul 2020 17:19:16 +0200
Subject: [PATCH] test: do not ignore whitespace in diff

It doesn't look like we were relying on it much
---
 tests/common.sh                     | 2 +-
 tests/compiler/t2.lean.expected.out | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/tests/common.sh b/tests/common.sh
index e7fa3e2544..2aaf6c13bd 100644
--- a/tests/common.sh
+++ b/tests/common.sh
@@ -40,7 +40,7 @@ function exec_check {
 
 function diff_produced {
     if test -f "$f.expected.out"; then
-        if $DIFF -u --ignore-all-space -I "executing external script" "$f.expected.out" "$f.produced.out"; then
+        if $DIFF -u -I "executing external script" "$f.expected.out" "$f.produced.out"; then
             exit 0
         else
             echo "ERROR: file $f.produced.out does not match $f.expected.out"
diff --git a/tests/compiler/t2.lean.expected.out b/tests/compiler/t2.lean.expected.out
index 7cfa48727d..f21737e60d 100644
--- a/tests/compiler/t2.lean.expected.out
+++ b/tests/compiler/t2.lean.expected.out
@@ -4,4 +4,4 @@
 4 count: 420
 5 count: 2202
 6 count: 12886
-7 count: 83648
\ No newline at end of file
+7 count: 83648