From 76da07e11f6a97a80ca5d420bfac218a849f39d1 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Thu, 2 May 2024 22:14:17 +1000
Subject: [PATCH] no need for trim

---
 test.sh | 17 -----------------
 1 file changed, 17 deletions(-)

diff --git a/test.sh b/test.sh
index dcfc341..0629d35 100755
--- a/test.sh
+++ b/test.sh
@@ -2,19 +2,6 @@
 
 lake build
 
-trim() {
-    local var="$*"
-    # Remove all leading whitespace and newline characters
-    while [[ $var =~ ^[[:space:]] ]]; do
-        var="${var#?}"  # Remove the first character repeatedly if it's whitespace
-    done
-    # Remove all trailing whitespace and newline characters
-    while [[ $var =~ [[:space:]]$ ]]; do
-        var="${var%?}"  # Remove the last character repeatedly if it's whitespace
-    done
-    printf '%s' "$var"
-}
-
 check_command() {
     local cmd="$1"
     local expected="$2"
@@ -26,10 +13,6 @@ check_command() {
         exit 1
     fi
 
-    # Account for weird whitespace from lake
-    # https://leanprover.zulipchat.com/#narrow/stream/428973-nightly-testing/topic/Mathlib.20status.20updates/near/436249454
-    output=$(trim "$output")
-
     if [[ "$output" != "$expected" ]]; then
         echo "Error: The command '$cmd' did not produce the expected error."
         echo "Expected:"