From 57cdda5821dc79d45ca426f19115e5c3c5d5c804 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 29 Oct 2019 13:37:38 -0700
Subject: [PATCH] chore: trying fix

---
 tests/compiler/test_single_interpret.sh | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/tests/compiler/test_single_interpret.sh b/tests/compiler/test_single_interpret.sh
index 5f872df372..c867b875f3 100755
--- a/tests/compiler/test_single_interpret.sh
+++ b/tests/compiler/test_single_interpret.sh
@@ -25,21 +25,21 @@ if diff --color --help >/dev/null 2>&1; then
   DIFF="diff --color";
 fi
 
-$LEAN --run "$ff" > "$ff.produced.out"
+$LEAN --run "$ff" > "$ff.interp.produced.out"
 if [ $? -ne 0 ]; then
    echo "Failed to execute $ff"
    exit 1
 fi
 
 if test -f "$ff.expected.out"; then
-    if $DIFF -u --ignore-all-space -I "executing external script" "$ff.expected.out" "$ff.produced.out"; then
+    if $DIFF -u --ignore-all-space -I "executing external script" "$ff.expected.out" "$ff.interp.produced.out"; then
         echo "-- checked"
         exit 0
     else
-        echo "ERROR: file $ff.produced.out does not match $ff.expected.out"
+        echo "ERROR: file $ff.interp.produced.out does not match $ff.expected.out"
         if [ $INTERACTIVE == "yes" ]; then
-            meld "$ff.produced.out" "$ff.expected.out"
-            if diff -I "executing external script" "$ff.expected.out" "$ff.produced.out"; then
+            meld "$ff.interp.produced.out" "$ff.expected.out"
+            if diff -I "executing external script" "$ff.expected.out" "$ff.interp.produced.out"; then
                 echo "-- mismatch was fixed"
             fi
         fi
@@ -48,10 +48,10 @@ if test -f "$ff.expected.out"; then
 else
     echo "ERROR: file $ff.expected.out does not exist"
     if [ $INTERACTIVE == "yes" ]; then
-        read -p "copy $ff.produced.out (y/n)? "
+        read -p "copy $ff.interp.produced.out (y/n)? "
         if [ $REPLY == "y" ]; then
-            cp -- "$ff.produced.out" "$ff.expected.out"
-            echo "-- copied $ff.produced.out --> $ff.expected.out"
+            cp -- "$ff.interp.produced.out" "$ff.expected.out"
+            echo "-- copied $ff.interp.produced.out --> $ff.expected.out"
         fi
     fi
     exit 1