From 72ccc09ee0d41caf06b50a407c340b80f65ee42b Mon Sep 17 00:00:00 2001 From: Max Date: Tue, 7 Jun 2022 16:24:54 -0400 Subject: [PATCH] remove file --- do_sed.sh | 12 ------------ 1 file changed, 12 deletions(-) delete mode 100755 do_sed.sh diff --git a/do_sed.sh b/do_sed.sh deleted file mode 100755 index 46e0878..0000000 --- a/do_sed.sh +++ /dev/null @@ -1,12 +0,0 @@ -#! /bin/sh - -srcs=`find lib include -name '*.c' -o -name '*.h' -o -name '*.cc'` -files=`grep -l 'boost.*shared_ptr' $srcs` - -dir=`pwd` - -for f in $files; do - echo editing file $f in $dir - sed -i 's%boost/shared_ptr.hpp%memory%' $f - sed -i 's%boost::shared_ptr%std::shared_ptr%' $f -done