Skip to content

Commit

Permalink
no need for trim
Browse files Browse the repository at this point in the history
  • Loading branch information
kim-em committed May 2, 2024
1 parent b68e32c commit 76da07e
Showing 1 changed file with 0 additions and 17 deletions.
17 changes: 0 additions & 17 deletions test.sh
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand All @@ -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:"
Expand Down

0 comments on commit 76da07e

Please sign in to comment.