remove unused sed routine

rjust · Jun 21, 2024 · 39a9a82 · 39a9a82
1 parent a07e3d5
commit 39a9a82
Showing 1 changed file with 0 additions and 9 deletions.
diff --git a/framework/test/test_verify_bugs.sh b/framework/test/test_verify_bugs.sh
@@ -102,15 +102,6 @@ mkdir -p $DIR_FAILING
 
 work_dir="$test_dir/$PID"
 
-function sed_cmd()
-{
-    if [ $(uname -s) = "Darwin" ]; then
-        sed -i '' "$1" $2
-    else
-        sed -i "$1" $2
-    fi
-}
-
 # Clean working directory
 rm -rf $work_dir
 for bid in $(echo $BUGS); do